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

Theorem rexeqi 2916
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 2912 . 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 set class
Syntax hints:    <-> wb 178    = wceq 1654   E.wrex 2713
This theorem is referenced by:  rexrab2  3111  rexprg  3887  rextpg  3889  rexxp  5052  oarec  6841  4sqlem12  13362  cmpfi  17509  txbas  17637  xkobval  17656  ustn0  18288  imasdsf1olem  18441  xpsdsval  18449  plyun0  20154  coeeu  20182  1cubr  20720  nbgraf1olem1  21489  adjbdln  23624  elunirnmbfm  24638  nofulllem5  25696  filnetlem4  26452  rexrabdioph  26966  fnwe2lem2  27238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2718
  Copyright terms: Public domain W3C validator