Theorem rexeqi 3297

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

Syntax hints:   ↔ wb 206   = wceq 1542  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-rex 3063

This theorem is referenced by:  rexrab2  3660  rexprgf  4654  rextpg  4658  rexopabb  5484  rexxp  5799  elidinxpid  6012  elrid  6013  oarec  8499  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  wwlktovfo  14893  dvdsprmpweqnn  16825  4sqlem12  16896  pzriprnglem10  21457  pmatcollpw3fi1  22744  cmpfi  23364  txbas  23523  xkobval  23542  ustn0  24177  imasdsf1olem  24329  xpsdsval  24337  plyun0  26170  coeeu  26198  1cubr  26820  made0  27871  addsrid  27972  muls01  28120  mulsrid  28121  precsexlemcbv  28214  dfnbgr3  29423  wlkvtxedg  29729  wwlksn0  29948  eucrctshift  30330  adjbdln  32170  elunirnmbfm  34429  onvf1odlem2  35317  satfbrsuc  35579  fmla1  35600  satffunlem2lem2  35619  filnetlem4  36594  rexrabdioph  43148  fnwe2lem2  43405  fourierdlem70  46531  fourierdlem80  46541  dfclnbgr3  48183  stgr1  48318