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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-rex 3091

This theorem is used by:  rexrab2  3661  rexprgf  4656  rextpg  4660  rexopabb  5507  rexxp  5826  elidinxpid  6050  elrid  6051  fnwe2lem3  8177  oarec  8601  brttrcl2  9745  ttrcltr  9747  rnttrcl  9753  wwlktovfo  15143  dvdsprmpweqnn  17095  4sqlem12  17166  pzriprnglem10  21829  pmatcollpw3fi1  23139  cmpfi  23759  txbas  23919  xkobval  23938  ustn0  24573  imasdsf1olem  24725  xpsdsval  24733  plyun0  26548  coeeu  26577  1cubr  27203  made0  28282  addsrid  28383  muls01  28531  mulsrid  28532  precsexlemcbv  28625  dfnbgr3  29952  wlkvtxedg  30257  wwlksn0  30485  eucrctshift  30877  adjbdln  32718  elunirnmbfm  34968  acwer1prc  35865  onvf1odlem2  36045  satfbrsuc  36311  fmla1  36332  satffunlem2lem2  36351  filnetlem4  37360  rexrabdioph  44005  fourierdlem70  47401  fourierdlem80  47411  dfclnbgr3  49139  stgr1  49274