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

Step	Hyp	Ref	Expression
1		raleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		rexeq 3116	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)

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