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

Theorem rexeqi 3329
 Description: Equality inference for restricted existential quantifier. (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 3325 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1539  ∃wrex 3072 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-clel 2831  df-rex 3077 This theorem is referenced by:  rexrab2  3617  rexprgf  4589  rextpg  4593  rexopabb  5386  rexxp  5683  elidinxpid  5885  elrid  5886  oarec  8199  wwlktovfo  14370  dvdsprmpweqnn  16277  4sqlem12  16348  pmatcollpw3fi1  21489  cmpfi  22109  txbas  22268  xkobval  22287  ustn0  22922  imasdsf1olem  23076  xpsdsval  23084  plyun0  24894  coeeu  24922  1cubr  25528  dfnbgr3  27228  wlkvtxedg  27533  wwlksn0  27749  eucrctshift  28128  adjbdln  29966  elunirnmbfm  31740  satfbrsuc  32845  fmla1  32866  satffunlem2lem2  32885  made0  33615  addsid1  33676  filnetlem4  34120  rexrabdioph  40109  fnwe2lem2  40369  fourierdlem70  43185  fourierdlem80  43195
 Copyright terms: Public domain W3C validator