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

Theorem ralbii2 2733
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 1575 . 2  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  B  ->  ps ) )
3 df-ral 2710 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2710 . 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 1549    e. wcel 1725   A.wral 2705
This theorem is referenced by:  raleqbii  2735  ralbiia  2737  ralrab  3096  raldifb  3487  reusv2  4729  dfsup2  7447  iscard2  7863  acnnum  7933  dfac9  8016  dfacacn  8021  raluz2  10526  ralrp  10630  isprm4  13089  isdomn2  16359  isnrm2  17422  ismbl  19422  ellimc3  19766  dchrelbas2  21021  h1dei  23052  raldifsni  26734  fnwe2lem2  27126  sdrgacs  27486
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ral 2710
  Copyright terms: Public domain W3C validator