Theorem rexeqi 3333

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

Syntax hints:   ↔ wb 206   = wceq 1537  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-rex 3077

This theorem is referenced by:  rexrab2  3722  rexprgf  4718  rextpg  4724  rexopabb  5547  rexxp  5867  elidinxpid  6074  elrid  6075  oarec  8618  brttrcl2  9783  ttrcltr  9785  rnttrcl  9791  wwlktovfo  15007  dvdsprmpweqnn  16932  4sqlem12  17003  pzriprnglem10  21524  pmatcollpw3fi1  22815  cmpfi  23437  txbas  23596  xkobval  23615  ustn0  24250  imasdsf1olem  24404  xpsdsval  24412  plyun0  26256  coeeu  26284  1cubr  26903  made0  27930  addsrid  28015  muls01  28156  mulsrid  28157  precsexlemcbv  28248  dfnbgr3  29373  wlkvtxedg  29680  wwlksn0  29896  eucrctshift  30275  adjbdln  32115  elunirnmbfm  34216  satfbrsuc  35334  fmla1  35355  satffunlem2lem2  35374  filnetlem4  36347  rexrabdioph  42750  fnwe2lem2  43008  fourierdlem70  46097  fourierdlem80  46107  dfclnbgr3  47699