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

Theorem rexeqi 3063
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 3059 . 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 1379   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820
This theorem is referenced by:  rexrab2  3271  rexprg  4077  rextpg  4079  rexxp  5145  oarec  7211  wwlktovfo  12859  4sqlem12  14333  pmatcollpw3fi1  19084  cmpfi  19702  txbas  19831  xkobval  19850  ustn0  20486  imasdsf1olem  20639  xpsdsval  20647  plyun0  22357  coeeu  22385  1cubr  22929  nbgraf1olem1  24145  wlknwwlknsur  24416  wlkiswwlksur  24423  adjbdln  26706  elunirnmbfm  27892  nofulllem5  29071  filnetlem4  29830  rexrabdioph  30359  fnwe2lem2  30629
  Copyright terms: Public domain W3C validator