Theorem rexeqi 3298

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rexrab2  3671  rexprgf  4659  rextpg  4663  rexopabb  5488  rexxp  5806  elidinxpid  6016  elrid  6017  oarec  8526  brttrcl2  9667  ttrcltr  9669  rnttrcl  9675  wwlktovfo  14924  dvdsprmpweqnn  16856  4sqlem12  16927  pzriprnglem10  21400  pmatcollpw3fi1  22675  cmpfi  23295  txbas  23454  xkobval  23473  ustn0  24108  imasdsf1olem  24261  xpsdsval  24269  plyun0  26102  coeeu  26130  1cubr  26752  made0  27785  addsrid  27871  muls01  28015  mulsrid  28016  precsexlemcbv  28108  dfnbgr3  29265  wlkvtxedg  29572  wwlksn0  29793  eucrctshift  30172  adjbdln  32012  elunirnmbfm  34242  onvf1odlem2  35091  satfbrsuc  35353  fmla1  35374  satffunlem2lem2  35393  filnetlem4  36369  rexrabdioph  42782  fnwe2lem2  43040  fourierdlem70  46174  fourierdlem80  46184  dfclnbgr3  47827  stgr1  47960