Theorem rexeqi 3320

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

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-rex 3089

This theorem is used by:  rexrab2  3661  rexprgf  4659  rextpg  4663  rexopabb  5510  rexxp  5826  elidinxpid  6045  elrid  6046  oarec  8553  brttrcl2  9697  ttrcltr  9699  rnttrcl  9705  wwlktovfo  15035  dvdsprmpweqnn  16983  4sqlem12  17054  pzriprnglem10  21709  pmatcollpw3fi1  23019  cmpfi  23639  txbas  23799  xkobval  23818  ustn0  24453  imasdsf1olem  24605  xpsdsval  24613  plyun0  26429  coeeu  26458  1cubr  27087  made0  28136  addsrid  28237  muls01  28385  mulsrid  28386  precsexlemcbv  28479  dfnbgr3  29806  wlkvtxedg  30111  wwlksn0  30339  eucrctshift  30731  adjbdln  32572  elunirnmbfm  34771  onvf1odlem2  35709  satfbrsuc  35953  fmla1  35974  satffunlem2lem2  35993  filnetlem4  37008  rexrabdioph  43643  fnwe2lem2  43900  fourierdlem70  47012  fourierdlem80  47022  dfclnbgr3  48750  stgr1  48885