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

Theorem rexbii2 2932
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 1714 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2788 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2788 . 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 1659    e. wcel 1870   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-rex 2788
This theorem is referenced by:  rexbiia  2933  rexbii  2934  rexeqbii  2950  rexrab  3241  rexdifsn  4132  reusv2lem4  4629  reusv2  4631  wefrc  4848  wfi  5432  bnd2  8363  rexuz2  11210  rexrp  11322  rexuz3  13390  infpn2  14820  efgrelexlemb  17335  cmpcov2  20336  cmpfi  20354  subislly  20427  txkgen  20598  cubic  23640  sumdmdii  27903  pcmplfin  28526  bnj882  29525  bnj893  29527  frind  30268  heibor1  31845  prtlem100  32134  islmodfg  35632  limcrecl  37280  rexdifpr  38376
  Copyright terms: Public domain W3C validator