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

Theorem rexeqi 3135
 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 3131 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   = wceq 1480  ∃wrex 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913 This theorem is referenced by:  rexrab2  3360  rexprg  4211  rextpg  4213  rexxp  5229  oarec  7594  wwlktovfo  13643  dvdsprmpweqnn  15524  4sqlem12  15595  pmatcollpw3fi1  20525  cmpfi  21134  txbas  21293  xkobval  21312  ustn0  21947  imasdsf1olem  22101  xpsdsval  22109  plyun0  23874  coeeu  23902  1cubr  24486  wwlksn0  26634  wlknwwlksnsur  26662  wlkwwlksur  26669  eucrctshift  26986  adjbdln  28812  elunirnmbfm  30120  filnetlem4  32053  rexrabdioph  36873  fnwe2lem2  37136  fourierdlem70  39726  fourierdlem80  39736
 Copyright terms: Public domain W3C validator