Theorem rexeqi 3295

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 3292	. 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  3647  rexprgf  4640  rextpg  4644  rexopabb  5476  rexxp  5791  elidinxpid  6004  elrid  6005  oarec  8490  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  wwlktovfo  14911  dvdsprmpweqnn  16847  4sqlem12  16918  pzriprnglem10  21480  pmatcollpw3fi1  22763  cmpfi  23383  txbas  23542  xkobval  23561  ustn0  24196  imasdsf1olem  24348  xpsdsval  24356  plyun0  26172  coeeu  26200  1cubr  26819  made0  27869  addsrid  27970  muls01  28118  mulsrid  28119  precsexlemcbv  28212  dfnbgr3  29421  wlkvtxedg  29727  wwlksn0  29946  eucrctshift  30328  adjbdln  32169  elunirnmbfm  34412  onvf1odlem2  35302  satfbrsuc  35564  fmla1  35585  satffunlem2lem2  35604  filnetlem4  36579  rexrabdioph  43240  fnwe2lem2  43497  fourierdlem70  46622  fourierdlem80  46632  dfclnbgr3  48314  stgr1  48449