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

Theorem ralbidv2 2892
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 1684 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  <->  A. x ( x  e.  B  ->  ch ) ) )
3 df-ral 2812 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2812 . 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 1372    e. wcel 1762   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675
This theorem depends on definitions:  df-bi 185  df-ral 2812
This theorem is referenced by:  ralbidva  2893  ralss  3559  oneqmini  4922  ordunisuc2  6650  dfsmo2  7008  wemapsolem  7964  zorn2lem1  8865  raluz  11118  limsupgle  13249  ello12  13288  elo12  13299  lo1resb  13336  rlimresb  13337  o1resb  13338  isprm3  14074  ist1  19581  ist1-2  19607  hausdiag  19874  xkopt  19884  cnflf  20231  cnfcf  20271  metcnp  20772  caucfil  21450  mdegleb  22192  eulerpartlemgvv  27941  filnetlem4  29789
  Copyright terms: Public domain W3C validator