Theorem rexeqi 3304

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-rex 3061

This theorem is referenced by:  rexrab2  3683  rexprgf  4671  rextpg  4675  rexopabb  5503  rexxp  5822  elidinxpid  6032  elrid  6033  oarec  8574  brttrcl2  9728  ttrcltr  9730  rnttrcl  9736  wwlktovfo  14977  dvdsprmpweqnn  16905  4sqlem12  16976  pzriprnglem10  21451  pmatcollpw3fi1  22726  cmpfi  23346  txbas  23505  xkobval  23524  ustn0  24159  imasdsf1olem  24312  xpsdsval  24320  plyun0  26154  coeeu  26182  1cubr  26804  made0  27837  addsrid  27923  muls01  28067  mulsrid  28068  precsexlemcbv  28160  dfnbgr3  29317  wlkvtxedg  29624  wwlksn0  29845  eucrctshift  30224  adjbdln  32064  elunirnmbfm  34283  satfbrsuc  35388  fmla1  35409  satffunlem2lem2  35428  filnetlem4  36399  rexrabdioph  42817  fnwe2lem2  43075  fourierdlem70  46205  fourierdlem80  46215  dfclnbgr3  47840  stgr1  47973