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

Theorem rexeqi 3280
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 3276 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1630  wrex 3049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rex 3054
This theorem is referenced by:  rexrab2  3513  rexprg  4377  rextpg  4379  rexxp  5418  oarec  7809  wwlktovfo  13900  dvdsprmpweqnn  15789  4sqlem12  15860  pmatcollpw3fi1  20793  cmpfi  21411  txbas  21570  xkobval  21589  ustn0  22223  imasdsf1olem  22377  xpsdsval  22385  plyun0  24150  coeeu  24178  1cubr  24766  dfnbgr3  26428  wlkvtxedg  26748  wwlksn0  26970  wlknwwlksnsur  26997  wlkwwlksur  27004  eucrctshift  27393  adjbdln  29249  elunirnmbfm  30622  filnetlem4  32680  rexrabdioph  37858  fnwe2lem2  38121  fourierdlem70  40894  fourierdlem80  40904
  Copyright terms: Public domain W3C validator