Theorem rexeqi 3322

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

Syntax hints:   ↔ wb 209   = wceq 1563  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-rex 3090

This theorem is referenced by:  rexrab2  3666  rexprgf  4657  rextpg  4661  rexopabb  5503  rexxp  5819  elidinxpid  6038  elrid  6039  oarec  8535  brttrcl2  9671  ttrcltr  9673  rnttrcl  9679  wwlktovfo  14985  dvdsprmpweqnn  16935  4sqlem12  17006  pzriprnglem10  21600  pmatcollpw3fi1  22906  cmpfi  23526  txbas  23685  xkobval  23704  ustn0  24339  imasdsf1olem  24491  xpsdsval  24499  plyun0  26315  coeeu  26343  1cubr  26965  made0  28014  addsrid  28115  muls01  28263  mulsrid  28264  precsexlemcbv  28357  dfnbgr3  29597  wlkvtxedg  29902  wwlksn0  30121  eucrctshift  30503  adjbdln  32344  elunirnmbfm  34559  onvf1odlem2  35459  satfbrsuc  35729  fmla1  35750  satffunlem2lem2  35769  filnetlem4  36754  rexrabdioph  43383  fnwe2lem2  43640  fourierdlem70  46748  fourierdlem80  46758  dfclnbgr3  48446  stgr1  48581