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

Theorem rexbii2 2736
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 1593 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2713 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2713 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 270 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  rexeqbii  2738  rexbiia  2740  rexrab  3100  rexdifsn  3933  wefrc  4579  reusv2lem4  4730  reusv2  4732  bnd2  7822  rexuz2  10533  rexrp  10636  rexuz3  12157  infpn2  13286  efgrelexlemb  15387  cmpcov2  17458  cmpfi  17476  subislly  17549  txkgen  17689  cubic  20694  sumdmdii  23923  wfi  25487  frind  25523  heibor1  26533  prtlem100  26718  islmodfg  27158  rexdifpr  28073  bnj882  29371  bnj893  29373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-rex 2713
  Copyright terms: Public domain W3C validator