Theorem rexeqi 3300

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

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

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 2702

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

This theorem is referenced by:  rexrab2  3674  rexprgf  4662  rextpg  4666  rexopabb  5491  rexxp  5809  elidinxpid  6019  elrid  6020  oarec  8529  brttrcl2  9674  ttrcltr  9676  rnttrcl  9682  wwlktovfo  14931  dvdsprmpweqnn  16863  4sqlem12  16934  pzriprnglem10  21407  pmatcollpw3fi1  22682  cmpfi  23302  txbas  23461  xkobval  23480  ustn0  24115  imasdsf1olem  24268  xpsdsval  24276  plyun0  26109  coeeu  26137  1cubr  26759  made0  27792  addsrid  27878  muls01  28022  mulsrid  28023  precsexlemcbv  28115  dfnbgr3  29272  wlkvtxedg  29579  wwlksn0  29800  eucrctshift  30179  adjbdln  32019  elunirnmbfm  34249  onvf1odlem2  35098  satfbrsuc  35360  fmla1  35381  satffunlem2lem2  35400  filnetlem4  36376  rexrabdioph  42789  fnwe2lem2  43047  fourierdlem70  46181  fourierdlem80  46191  dfclnbgr3  47831  stgr1  47964