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 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-rex 3071

This theorem is referenced by:  rexrab2  3706  rexprgf  4695  rextpg  4699  rexopabb  5533  rexxp  5853  elidinxpid  6063  elrid  6064  oarec  8600  brttrcl2  9754  ttrcltr  9756  rnttrcl  9762  wwlktovfo  14997  dvdsprmpweqnn  16923  4sqlem12  16994  pzriprnglem10  21501  pmatcollpw3fi1  22794  cmpfi  23416  txbas  23575  xkobval  23594  ustn0  24229  imasdsf1olem  24383  xpsdsval  24391  plyun0  26236  coeeu  26264  1cubr  26885  made0  27912  addsrid  27997  muls01  28138  mulsrid  28139  precsexlemcbv  28230  dfnbgr3  29355  wlkvtxedg  29662  wwlksn0  29883  eucrctshift  30262  adjbdln  32102  elunirnmbfm  34253  satfbrsuc  35371  fmla1  35392  satffunlem2lem2  35411  filnetlem4  36382  rexrabdioph  42805  fnwe2lem2  43063  fourierdlem70  46191  fourierdlem80  46201  dfclnbgr3  47813  stgr1  47928