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

Theorem rexeqi 2853
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 2849 . 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 1649   E.wrex 2651
This theorem is referenced by:  rexrab2  3046  rexprg  3802  rextpg  3804  rexxp  4958  oarec  6742  4sqlem12  13252  cmpfi  17394  txbas  17521  xkobval  17540  ustn0  18172  imasdsf1olem  18312  xpsdsval  18320  plyun0  19984  coeeu  20012  1cubr  20550  nbgraf1olem1  21318  adjbdln  23435  elunirnmbfm  24398  nofulllem5  25385  filnetlem4  26102  rexrabdioph  26546  fnwe2lem2  26818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656
  Copyright terms: Public domain W3C validator