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

Theorem ralbii2 2694
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 1572 . 2  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  B  ->  ps ) )
3 df-ral 2671 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2671 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43bitr4i 269 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    e. wcel 1721   A.wral 2666
This theorem is referenced by:  raleqbii  2696  ralbiia  2698  ralrab  3056  raldifb  3447  reusv2  4688  dfsup2  7405  iscard2  7819  acnnum  7889  dfac9  7972  dfacacn  7977  raluz2  10482  ralrp  10586  isprm4  13044  isdomn2  16314  isnrm2  17376  ismbl  19375  ellimc3  19719  dchrelbas2  20974  h1dei  23005  raldifsni  26624  fnwe2lem2  27016  sdrgacs  27377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ral 2671
  Copyright terms: Public domain W3C validator