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

Theorem rexeqi 2901
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 2897 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
31, 2ax-mp 8 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652   E.wrex 2698
This theorem is referenced by:  rexrab2  3094  rexprg  3850  rextpg  3852  rexxp  5008  oarec  6796  4sqlem12  13312  cmpfi  17459  txbas  17587  xkobval  17606  ustn0  18238  imasdsf1olem  18391  xpsdsval  18399  plyun0  20104  coeeu  20132  1cubr  20670  nbgraf1olem1  21439  adjbdln  23574  elunirnmbfm  24591  nofulllem5  25615  filnetlem4  26347  rexrabdioph  26791  fnwe2lem2  27063
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703
  Copyright terms: Public domain W3C validator