Theorem rexeqi 3318

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-rex 3087

This theorem is used by:  rexrab2  3657  rexprgf  4652  rextpg  4656  rexopabb  5501  rexxp  5818  elidinxpid  6036  elrid  6037  fnwe2lem3  8150  oarec  8574  brttrcl2  9719  ttrcltr  9721  rnttrcl  9727  wwlktovfo  15117  dvdsprmpweqnn  17069  4sqlem12  17140  pzriprnglem10  21802  pmatcollpw3fi1  23112  cmpfi  23732  txbas  23892  xkobval  23911  ustn0  24546  imasdsf1olem  24698  xpsdsval  24706  plyun0  26521  coeeu  26550  1cubr  27176  made0  28255  addsrid  28356  muls01  28504  mulsrid  28505  precsexlemcbv  28598  dfnbgr3  29925  wlkvtxedg  30230  wwlksn0  30458  eucrctshift  30850  adjbdln  32691  elunirnmbfm  34932  acwer1prc  35817  onvf1odlem2  35952  satfbrsuc  36218  fmla1  36239  satffunlem2lem2  36258  filnetlem4  37262  rexrabdioph  43895  fourierdlem70  47280  fourierdlem80  47290  dfclnbgr3  49018  stgr1  49153