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

Theorem rexbii2 2859
Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)
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 . . . 4  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  B  /\  ps )
)
21a1i 11 . . 3  |-  ( T. 
->  ( ( x  e.  A  /\  ph )  <->  ( x  e.  B  /\  ps ) ) )
32rexbidv2 2858 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
)
43trud 1379 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   T. wtru 1371    e. wcel 1758   E.wrex 2800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-tru 1373  df-ex 1588  df-rex 2805
This theorem is referenced by:  rexbiia  2861  rexbii  2862  rexeqbii  2872  rexrab  3230  rexdifsn  4115  reusv2lem4  4607  reusv2  4609  wefrc  4825  bnd2  8215  rexuz2  11021  rexrp  11125  rexuz3  12958  infpn2  14096  efgrelexlemb  16372  cmpcov2  19135  cmpfi  19153  subislly  19227  txkgen  19367  cubic  22387  sumdmdii  25998  wfi  27835  frind  27871  heibor1  28880  prtlem100  29171  islmodfg  29593  rexdifpr  30295  bnj882  32274  bnj893  32276
  Copyright terms: Public domain W3C validator