Theorem rexeqi 3318

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

Syntax hints:   ↔ wb 208   = wceq 1559  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-rex 3086

This theorem is referenced by:  rexrab2  3662  rexprgf  4653  rextpg  4657  rexopabb  5497  rexxp  5812  elidinxpid  6031  elrid  6032  oarec  8526  brttrcl2  9666  ttrcltr  9668  rnttrcl  9674  wwlktovfo  14968  dvdsprmpweqnn  16904  4sqlem12  16975  pzriprnglem10  21522  pmatcollpw3fi1  22828  cmpfi  23448  txbas  23607  xkobval  23626  ustn0  24261  imasdsf1olem  24413  xpsdsval  24421  plyun0  26237  coeeu  26265  1cubr  26884  made0  27933  addsrid  28034  muls01  28182  mulsrid  28183  precsexlemcbv  28276  dfnbgr3  29485  wlkvtxedg  29790  wwlksn0  30009  eucrctshift  30391  adjbdln  32232  elunirnmbfm  34510  onvf1odlem2  35411  satfbrsuc  35680  fmla1  35701  satffunlem2lem2  35720  filnetlem4  36705  rexrabdioph  43335  fnwe2lem2  43592  fourierdlem70  46714  fourierdlem80  46724  dfclnbgr3  48412  stgr1  48547