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

Theorem rexbii2 2898
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 1728 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2754 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2754 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 285 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375   E.wex 1673    e. wcel 1897   E.wrex 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692
This theorem depends on definitions:  df-bi 190  df-ex 1674  df-rex 2754
This theorem is referenced by:  rexbiia  2899  rexbii  2900  rexeqbii  2916  rexrab  3213  rexdifsn  4113  reusv2lem4  4620  reusv2  4622  wefrc  4846  wfi  5431  bnd2  8389  rexuz2  11238  rexrp  11350  rexuz3  13459  infpn2  14905  efgrelexlemb  17448  cmpcov2  20453  cmpfi  20471  subislly  20544  txkgen  20715  cubic  23823  sumdmdii  28116  pcmplfin  28735  bnj882  29785  bnj893  29787  frind  30529  heibor1  32186  prtlem100  32473  islmodfg  35971  limcrecl  37746  rexdifpr  39033
  Copyright terms: Public domain W3C validator