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

Theorem ralbii2 2883
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 1645 . 2  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  B  ->  ps ) )
3 df-ral 2809 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2809 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43bitr4i 277 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1396    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-ral 2809
This theorem is referenced by:  ralbiia  2884  ralbii  2885  raleqbii  2899  ralrab  3258  raldifb  3630  raldifsni  4146  reusv2  4643  dfsup2  7894  iscard2  8348  acnnum  8424  dfac9  8507  dfacacn  8512  raluz2  11131  ralrp  11240  isprm4  14311  isdomn2  18143  isnrm2  20026  ismbl  22103  ellimc3  22449  dchrelbas2  23710  h1dei  26666  fnwe2lem2  31236  sdrgacs  31391
  Copyright terms: Public domain W3C validator