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

Theorem ralbidv2 2839
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 1734 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2759 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2759 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43bitr4g 288 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1403    e. wcel 1842   A.wral 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725
This theorem depends on definitions:  df-bi 185  df-ral 2759
This theorem is referenced by:  ralbidva  2840  ralss  3505  oneqmini  5461  ordunisuc2  6662  dfsmo2  7051  wemapsolem  8009  zorn2lem1  8908  raluz  11175  limsupgle  13449  ello12  13488  elo12  13499  lo1resb  13536  rlimresb  13537  o1resb  13538  isprm3  14435  ist1  20115  ist1-2  20141  hausdiag  20438  xkopt  20448  cnflf  20795  cnfcf  20835  metcnp  21336  caucfil  22014  mdegleb  22756  eulerpartlemgvv  28821  filnetlem4  30609  isprm7  36040  elbigo2  38683
  Copyright terms: Public domain W3C validator