MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralbidv2 Structured version   Unicode version

Theorem ralbidv2 2733
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
Hypothesis
Ref Expression
ralbidv2.1  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  B  ->  ch ) ) )
Assertion
Ref Expression
ralbidv2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)    B( x)

Proof of Theorem ralbidv2
StepHypRef Expression
1 ralbidv2.1 . . 3  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  B  ->  ch ) ) )
21albidv 1636 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2716 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2716 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43bitr4g 281 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    e. wcel 1727   A.wral 2711
This theorem is referenced by:  ralss  3395  oneqmini  4661  ordunisuc2  4853  dfsmo2  6638  wemapso2lem  7548  zorn2lem1  8407  raluz  10556  limsupgle  12302  ello12  12341  elo12  12352  lo1resb  12389  rlimresb  12390  o1resb  12391  isprm3  13119  ist1  17416  ist1-2  17442  hausdiag  17708  xkopt  17718  cnflf  18065  cnfcf  18105  metcnp  18602  caucfil  19267  mdegleb  20018  filnetlem4  26448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-ral 2716
  Copyright terms: Public domain W3C validator