Theorem rexeqi 3319

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 3316	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)

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

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 2733

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

This theorem is used by:  rexrab2  3658  rexprgf  4656  rextpg  4660  rexopabb  5502  rexxp  5819  elidinxpid  6039  elrid  6040  oarec  8554  brttrcl2  9699  ttrcltr  9701  rnttrcl  9707  wwlktovfo  15091  dvdsprmpweqnn  17043  4sqlem12  17114  pzriprnglem10  21776  pmatcollpw3fi1  23086  cmpfi  23706  txbas  23866  xkobval  23885  ustn0  24520  imasdsf1olem  24672  xpsdsval  24680  plyun0  26495  coeeu  26524  1cubr  27152  made0  28231  addsrid  28332  muls01  28480  mulsrid  28481  precsexlemcbv  28574  dfnbgr3  29901  wlkvtxedg  30206  wwlksn0  30434  eucrctshift  30826  adjbdln  32667  elunirnmbfm  34867  onvf1odlem2  35856  satfbrsuc  36100  fmla1  36121  satffunlem2lem2  36140  filnetlem4  37139  rexrabdioph  43754  fnwe2lem2  44011  fourierdlem70  47130  fourierdlem80  47140  dfclnbgr3  48868  stgr1  49003