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

Theorem ralbii2 2834
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 1611 . 2  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  B  ->  ps ) )
3 df-ral 2801 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2801 . 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 1368    e. wcel 1758   A.wral 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ral 2801
This theorem is referenced by:  ralbiia  2835  ralbii  2836  raleqbii  2845  ralrab  3222  raldifb  3599  raldifsni  4108  reusv2  4601  dfsup2  7798  iscard2  8252  acnnum  8328  dfac9  8411  dfacacn  8416  raluz2  11010  ralrp  11115  isprm4  13886  isdomn2  17489  isnrm2  19089  ismbl  21136  ellimc3  21482  dchrelbas2  22704  h1dei  25100  fnwe2lem2  29547  sdrgacs  29701
  Copyright terms: Public domain W3C validator