Theorem rexeqi 3325

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-rex 3093

This theorem is used by:  rexrab2  3666  rexprgf  4666  rextpg  4670  rexopabb  5517  rexxp  5833  elidinxpid  6052  elrid  6053  oarec  8556  brttrcl2  9693  ttrcltr  9695  rnttrcl  9701  wwlktovfo  15021  dvdsprmpweqnn  16970  4sqlem12  17041  pzriprnglem10  21677  pmatcollpw3fi1  22982  cmpfi  23602  txbas  23761  xkobval  23780  ustn0  24415  imasdsf1olem  24567  xpsdsval  24575  plyun0  26391  coeeu  26419  1cubr  27044  made0  28093  addsrid  28194  muls01  28342  mulsrid  28343  precsexlemcbv  28436  dfnbgr3  29725  wlkvtxedg  30030  wwlksn0  30249  eucrctshift  30631  adjbdln  32472  elunirnmbfm  34674  onvf1odlem2  35612  satfbrsuc  35879  fmla1  35900  satffunlem2lem2  35919  filnetlem4  36933  rexrabdioph  43562  fnwe2lem2  43819  fourierdlem70  46931  fourierdlem80  46941  dfclnbgr3  48632  stgr1  48767