Theorem rexeqi 3323

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

Syntax hints:   ↔ wb 205   = wceq 1541  ∃wrex 3069

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-rex 3070

This theorem is referenced by:  rexrab2  3692  rexprgf  4690  rextpg  4696  rexopabb  5521  rexxp  5834  elidinxpid  6034  elrid  6035  oarec  8545  brttrcl2  9691  ttrcltr  9693  rnttrcl  9699  wwlktovfo  14891  dvdsprmpweqnn  16800  4sqlem12  16871  pmatcollpw3fi1  22219  cmpfi  22841  txbas  23000  xkobval  23019  ustn0  23654  imasdsf1olem  23808  xpsdsval  23816  plyun0  25640  coeeu  25668  1cubr  26274  made0  27291  addsrid  27364  muls01  27482  mulsrid  27483  dfnbgr3  28460  wlkvtxedg  28766  wwlksn0  28982  eucrctshift  29361  adjbdln  31199  elunirnmbfm  33081  satfbrsuc  34188  fmla1  34209  satffunlem2lem2  34228  filnetlem4  35070  rexrabdioph  41303  fnwe2lem2  41564  fourierdlem70  44665  fourierdlem80  44675