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

Theorem ralbidv2 2641
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 1625 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2624 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2624 . 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 1540    e. wcel 1710   A.wral 2619
This theorem is referenced by:  ralss  3315  oneqmini  4522  ordunisuc2  4714  dfsmo2  6448  wemapso2lem  7352  zorn2lem1  8210  raluz  10356  limsupgle  12041  ello12  12080  elo12  12091  lo1resb  12128  rlimresb  12129  o1resb  12130  isprm3  12858  ist1  17149  ist1-2  17175  hausdiag  17439  xkopt  17449  cnflf  17793  cnfcf  17833  metcnp  18183  caucfil  18807  mdegleb  19548  filnetlem4  25654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ral 2624
  Copyright terms: Public domain W3C validator