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

Theorem rexbii2 2648
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 1582 . 2  |-  ( E. x ( x  e.  A  /\  ph )  <->  E. x ( x  e.  B  /\  ps )
)
3 df-rex 2625 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2625 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43bitr4i 268 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1541    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  rexeqbii  2650  rexbiia  2652  rexrab  3005  rexdifsn  3829  wefrc  4469  reusv2lem4  4620  reusv2  4622  bnd2  7653  rexuz2  10362  rexrp  10465  rexuz3  11928  infpn2  13057  efgrelexlemb  15158  cmpcov2  17223  cmpfi  17241  subislly  17313  txkgen  17452  cubic  20256  sumdmdii  23109  wfi  24765  frind  24801  heibor1  25857  prtlem100  26044  islmodfg  26490  bnj882  28720  bnj893  28722
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-rex 2625
  Copyright terms: Public domain W3C validator