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 1570  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

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

This theorem is referenced by:  rexrab2  3664  rexprgf  4662  rextpg  4666  rexopabb  5514  rexxp  5830  elidinxpid  6049  elrid  6050  oarec  8548  brttrcl2  9684  ttrcltr  9686  rnttrcl  9692  wwlktovfo  14997  dvdsprmpweqnn  16946  4sqlem12  17017  pzriprnglem10  21621  pmatcollpw3fi1  22926  cmpfi  23546  txbas  23705  xkobval  23724  ustn0  24359  imasdsf1olem  24511  xpsdsval  24519  plyun0  26335  coeeu  26363  1cubr  26988  made0  28037  addsrid  28138  muls01  28286  mulsrid  28287  precsexlemcbv  28380  dfnbgr3  29669  wlkvtxedg  29974  wwlksn0  30193  eucrctshift  30575  adjbdln  32416  elunirnmbfm  34623  onvf1odlem2  35569  satfbrsuc  35839  fmla1  35860  satffunlem2lem2  35879  filnetlem4  36873  rexrabdioph  43504  fnwe2lem2  43761  fourierdlem70  46873  fourierdlem80  46883  dfclnbgr3  48574  stgr1  48709