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

Theorem ralbidv2 2822
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 1766 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2741 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2741 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43bitr4g 292 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1441    e. wcel 1886   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757
This theorem depends on definitions:  df-bi 189  df-ral 2741
This theorem is referenced by:  ralbidva  2823  ralss  3494  oneqmini  5473  ordunisuc2  6668  dfsmo2  7063  wemapsolem  8062  zorn2lem1  8923  raluz  11204  limsupgle  13528  ello12  13573  elo12  13584  lo1resb  13621  rlimresb  13622  o1resb  13623  isprm3  14626  ist1  20330  ist1-2  20356  hausdiag  20653  xkopt  20663  cnflf  21010  cnfcf  21050  metcnp  21549  caucfil  22246  mdegleb  23006  eulerpartlemgvv  29202  filnetlem4  31030  isprm7  36654  hoidmvle  38416  elbigo2  40350
  Copyright terms: Public domain W3C validator