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

Theorem rexbii2 2703
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 1589 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2680 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2680 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 269 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    e. wcel 1721   E.wrex 2675
This theorem is referenced by:  rexeqbii  2705  rexbiia  2707  rexrab  3066  rexdifsn  3899  wefrc  4544  reusv2lem4  4694  reusv2  4696  bnd2  7781  rexuz2  10492  rexrp  10595  rexuz3  12115  infpn2  13244  efgrelexlemb  15345  cmpcov2  17415  cmpfi  17433  subislly  17505  txkgen  17645  cubic  20650  sumdmdii  23879  wfi  25429  frind  25465  heibor1  26417  prtlem100  26602  islmodfg  27043  rexdifpr  27955  bnj882  29015  bnj893  29017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-rex 2680
  Copyright terms: Public domain W3C validator