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

Theorem rexeqi 2912
Description: Equality inference for restricted existential qualifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypothesis
Ref Expression
raleq1i.1  |-  A  =  B
Assertion
Ref Expression
rexeqi  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ph )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem rexeqi
StepHypRef Expression
1 raleq1i.1 . 2  |-  A  =  B
2 rexeq 2908 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
31, 2ax-mp 5 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1362   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711
This theorem is referenced by:  rexrab2  3116  rexprg  3914  rextpg  3916  rexxp  4969  oarec  6989  4sqlem12  13999  cmpfi  18852  txbas  18981  xkobval  19000  ustn0  19636  imasdsf1olem  19789  xpsdsval  19797  plyun0  21549  coeeu  21577  1cubr  22121  nbgraf1olem1  23172  adjbdln  25309  elunirnmbfm  26521  nofulllem5  27693  filnetlem4  28443  rexrabdioph  28974  fnwe2lem2  29246  wwlktovfo  30096  wlknwwlknsur  30187  wlkiswwlksur  30194
  Copyright terms: Public domain W3C validator