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

Theorem ralbidv2 2696
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 1632 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2679 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2679 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43bitr4g 280 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    e. wcel 1721   A.wral 2674
This theorem is referenced by:  ralss  3377  oneqmini  4600  ordunisuc2  4791  dfsmo2  6576  wemapso2lem  7483  zorn2lem1  8340  raluz  10489  limsupgle  12234  ello12  12273  elo12  12284  lo1resb  12321  rlimresb  12322  o1resb  12323  isprm3  13051  ist1  17347  ist1-2  17373  hausdiag  17638  xkopt  17648  cnflf  17995  cnfcf  18035  metcnp  18532  caucfil  19197  mdegleb  19948  filnetlem4  26308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ral 2679
  Copyright terms: Public domain W3C validator