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

Theorem rexeqi 3120
 Description: Equality inference for restricted existential qualifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypothesis
Ref Expression
raleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
rexeqi (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeqi
StepHypRef Expression
1 raleq1i.1 . 2 𝐴 = 𝐵
2 rexeq 3116 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   = wceq 1475  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902 This theorem is referenced by:  rexrab2  3341  rexprg  4182  rextpg  4184  rexxp  5186  oarec  7529  wwlktovfo  13549  dvdsprmpweqnn  15427  4sqlem12  15498  pmatcollpw3fi1  20412  cmpfi  21021  txbas  21180  xkobval  21199  ustn0  21834  imasdsf1olem  21988  xpsdsval  21996  plyun0  23757  coeeu  23785  1cubr  24369  nbgraf1olem1  25970  wlknwwlknsur  26240  wlkiswwlksur  26247  adjbdln  28326  elunirnmbfm  29642  nofulllem5  31105  filnetlem4  31546  rexrabdioph  36376  fnwe2lem2  36639  fourierdlem70  39069  fourierdlem80  39079  wwlksn0  41059  wlknwwlksnsur  41087  wlkwwlksur  41094  eucrctshift  41411
 Copyright terms: Public domain W3C validator