Theorem rexeqi 3289

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rexrab2  3662  rexprgf  4649  rextpg  4653  rexopabb  5475  rexxp  5789  elidinxpid  6000  elrid  6001  oarec  8487  brttrcl2  9629  ttrcltr  9631  rnttrcl  9637  wwlktovfo  14883  dvdsprmpweqnn  16815  4sqlem12  16886  pzriprnglem10  21415  pmatcollpw3fi1  22691  cmpfi  23311  txbas  23470  xkobval  23489  ustn0  24124  imasdsf1olem  24277  xpsdsval  24285  plyun0  26118  coeeu  26146  1cubr  26768  made0  27805  addsrid  27894  muls01  28038  mulsrid  28039  precsexlemcbv  28131  dfnbgr3  29301  wlkvtxedg  29607  wwlksn0  29826  eucrctshift  30205  adjbdln  32045  elunirnmbfm  34221  onvf1odlem2  35079  satfbrsuc  35341  fmla1  35362  satffunlem2lem2  35381  filnetlem4  36357  rexrabdioph  42770  fnwe2lem2  43027  fourierdlem70  46161  fourierdlem80  46171  dfclnbgr3  47814  stgr1  47949