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

Theorem ralbii2 2584
Description: Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
Hypothesis
Ref Expression
ralbii2.1  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  B  ->  ps )
)
Assertion
Ref Expression
ralbii2  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ps )

Proof of Theorem ralbii2
StepHypRef Expression
1 ralbii2.1 . . 3  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  B  ->  ps )
)
21albii 1556 . 2  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  B  ->  ps ) )
3 df-ral 2561 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2561 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43bitr4i 268 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    e. wcel 1696   A.wral 2556
This theorem is referenced by:  raleqbii  2586  ralbiia  2588  ralrab  2940  reusv2  4556  dfsup2  7211  iscard2  7625  acnnum  7695  dfac9  7778  dfacacn  7783  raluz2  10284  ralrp  10388  isprm4  12784  isdomn2  16056  isnrm2  17102  ismbl  18901  ellimc3  19245  dchrelbas2  20492  h1dei  22145  wfrlem5  24331  frrlem5  24356  isoriso  25315  vecval1b  25554  vecval3b  25555  isntr  25976  raldifsni  26856  fnwe2lem2  27251  sdrgacs  27612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator