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

Theorem rexbii2 2858
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 1712 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2714 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2714 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 280 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wex 1657    e. wcel 1872   E.wrex 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-rex 2714
This theorem is referenced by:  rexbiia  2859  rexbii  2860  rexeqbii  2876  rexrab  3170  rexdifsn  4065  reusv2lem4  4564  reusv2  4566  wefrc  4783  wfi  5368  bnd2  8309  rexuz2  11154  rexrp  11266  rexuz3  13348  infpn2  14793  efgrelexlemb  17336  cmpcov2  20340  cmpfi  20358  subislly  20431  txkgen  20602  cubic  23710  sumdmdii  28003  pcmplfin  28632  bnj882  29682  bnj893  29684  frind  30425  heibor1  32043  prtlem100  32332  islmodfg  35834  limcrecl  37586  rexdifpr  38797
  Copyright terms: Public domain W3C validator