Theorem rexeqi 3294

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

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

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 2708

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

This theorem is referenced by:  rexrab2  3646  rexprgf  4639  rextpg  4643  rexopabb  5483  rexxp  5797  elidinxpid  6010  elrid  6011  oarec  8497  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  wwlktovfo  14920  dvdsprmpweqnn  16856  4sqlem12  16927  pzriprnglem10  21470  pmatcollpw3fi1  22753  cmpfi  23373  txbas  23532  xkobval  23551  ustn0  24186  imasdsf1olem  24338  xpsdsval  24346  plyun0  26162  coeeu  26190  1cubr  26806  made0  27855  addsrid  27956  muls01  28104  mulsrid  28105  precsexlemcbv  28198  dfnbgr3  29407  wlkvtxedg  29712  wwlksn0  29931  eucrctshift  30313  adjbdln  32154  elunirnmbfm  34396  onvf1odlem2  35286  satfbrsuc  35548  fmla1  35569  satffunlem2lem2  35588  filnetlem4  36563  rexrabdioph  43222  fnwe2lem2  43479  fourierdlem70  46604  fourierdlem80  46614  dfclnbgr3  48302  stgr1  48437