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

Theorem rexbii2 2954
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 1672 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2810 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2810 . 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 367   E.wex 1617    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-rex 2810
This theorem is referenced by:  rexbiia  2955  rexbii  2956  rexeqbii  2969  rexrab  3260  rexdifsn  4145  reusv2lem4  4641  reusv2  4643  wefrc  4862  bnd2  8302  rexuz2  11133  rexrp  11241  rexuz3  13266  infpn2  14518  efgrelexlemb  16970  cmpcov2  20060  cmpfi  20078  subislly  20151  txkgen  20322  cubic  23380  sumdmdii  27535  pcmplfin  28101  wfi  29530  frind  29566  heibor1  30549  prtlem100  30839  islmodfg  31257  limcrecl  31877  rexdifpr  32693  bnj882  34404  bnj893  34406
  Copyright terms: Public domain W3C validator