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

Theorem rexeqi 2943
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 2939 . 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 1369   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742
This theorem is referenced by:  rexrab2  3148  rexprg  3947  rextpg  3949  rexxp  5003  oarec  7022  4sqlem12  14038  cmpfi  19033  txbas  19162  xkobval  19181  ustn0  19817  imasdsf1olem  19970  xpsdsval  19978  plyun0  21687  coeeu  21715  1cubr  22259  nbgraf1olem1  23372  adjbdln  25509  elunirnmbfm  26690  nofulllem5  27869  filnetlem4  28628  rexrabdioph  29158  fnwe2lem2  29430  wwlktovfo  30279  wlknwwlknsur  30370  wlkiswwlksur  30377
  Copyright terms: Public domain W3C validator