Theorem rexeqi 3296

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

Syntax hints:   ↔ wb 207   = wceq 1547  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-rex 3064

This theorem is referenced by:  rexrab2  3641  rexprgf  4627  rextpg  4631  rexopabb  5470  rexxp  5784  elidinxpid  5997  elrid  5998  oarec  8487  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  wwlktovfo  14911  dvdsprmpweqnn  16847  4sqlem12  16918  pzriprnglem10  21465  pmatcollpw3fi1  22771  cmpfi  23391  txbas  23550  xkobval  23569  ustn0  24204  imasdsf1olem  24356  xpsdsval  24364  plyun0  26180  coeeu  26208  1cubr  26824  made0  27873  addsrid  27974  muls01  28122  mulsrid  28123  precsexlemcbv  28216  dfnbgr3  29425  wlkvtxedg  29730  wwlksn0  29949  eucrctshift  30331  adjbdln  32172  elunirnmbfm  34436  onvf1odlem2  35332  satfbrsuc  35594  fmla1  35615  satffunlem2lem2  35634  filnetlem4  36609  rexrabdioph  43239  fnwe2lem2  43496  fourierdlem70  46619  fourierdlem80  46629  dfclnbgr3  48317  stgr1  48452