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

Theorem rexbii2 2572
Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
Hypothesis
Ref Expression
rexbii2.1  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  B  /\  ps )
)
Assertion
Ref Expression
rexbii2  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )

Proof of Theorem rexbii2
StepHypRef Expression
1 rexbii2.1 . . 3  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  B  /\  ps )
)
21exbii 1569 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2549 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2549 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 268 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rexeqbii  2574  rexbiia  2576  rexrab  2929  rexdifsn  3753  wefrc  4387  reusv2lem4  4538  reusv2  4540  bnd2  7563  rexuz2  10270  rexrp  10373  rexuz3  11832  infpn2  12960  efgrelexlemb  15059  cmpcov2  17117  cmpfi  17135  subislly  17207  txkgen  17346  cubic  20145  sumdmdii  22995  wfi  24207  frind  24243  heibor1  26534  prtlem100  26721  islmodfg  27167  bnj882  28958  bnj893  28960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator