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

Theorem ralbii2 2817
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 1691 . 2  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  B  ->  ps ) )
3 df-ral 2742 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2742 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43bitr4i 281 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1442    e. wcel 1887   A.wral 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-ral 2742
This theorem is referenced by:  ralbiia  2818  ralbii  2819  raleqbii  2833  ralrab  3200  raldifb  3573  raldifsni  4102  reusv2  4609  dfsup2  7958  iscard2  8410  acnnum  8483  dfac9  8566  dfacacn  8571  raluz2  11208  ralrp  11321  isprm4  14634  isdomn2  18523  isnrm2  20374  ismbl  22480  ellimc3  22834  dchrelbas2  24165  h1dei  27203  fnwe2lem2  35909  sdrgacs  36067
  Copyright terms: Public domain W3C validator