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

Theorem ralbidv2 2565
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 1611 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2548 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2548 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43bitr4g 279 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralss  3239  oneqmini  4443  ordunisuc2  4635  dfsmo2  6364  wemapso2lem  7265  zorn2lem1  8123  raluz  10267  limsupgle  11951  ello12  11990  elo12  12001  lo1resb  12038  rlimresb  12039  o1resb  12040  isprm3  12767  ist1  17049  ist1-2  17075  hausdiag  17339  xkopt  17349  cnflf  17697  cnfcf  17737  metcnp  18087  caucfil  18709  mdegleb  19450  isorhom  25211  mxlelt  25264  iscom  25333  idlvalNEW  25445  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  isfuna  25834  isinob  25862  islimcat  25876  isibcg  26191  filnetlem4  26330
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator