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

Theorem rexbii2 2967
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 1644 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2823 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2823 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 277 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1596    e. wcel 1767   E.wrex 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-rex 2823
This theorem is referenced by:  rexbiia  2968  rexbii  2969  rexeqbii  2982  rexrab  3272  rexdifsn  4162  reusv2lem4  4657  reusv2  4659  wefrc  4879  bnd2  8323  rexuz2  11144  rexrp  11251  rexuz3  13161  infpn2  14307  efgrelexlemb  16641  cmpcov2  19758  cmpfi  19776  subislly  19850  txkgen  20021  cubic  23046  sumdmdii  27157  wfi  29214  frind  29250  heibor1  30233  prtlem100  30524  islmodfg  30943  rexdifpr  32090  bnj882  33464  bnj893  33466
  Copyright terms: Public domain W3C validator