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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

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

This theorem is referenced by:  rexrab2  3666  rexprgf  4657  rextpg  4661  rexopabb  5502  rexxp  5818  elidinxpid  6037  elrid  6038  oarec  8535  brttrcl2  9671  ttrcltr  9673  rnttrcl  9679  wwlktovfo  14983  dvdsprmpweqnn  16933  4sqlem12  17004  pzriprnglem10  21597  pmatcollpw3fi1  22902  cmpfi  23522  txbas  23681  xkobval  23700  ustn0  24335  imasdsf1olem  24487  xpsdsval  24495  plyun0  26311  coeeu  26339  1cubr  26961  made0  28010  addsrid  28111  muls01  28259  mulsrid  28260  precsexlemcbv  28353  dfnbgr3  29593  wlkvtxedg  29898  wwlksn0  30117  eucrctshift  30499  adjbdln  32340  elunirnmbfm  34554  onvf1odlem2  35454  satfbrsuc  35724  fmla1  35745  satffunlem2lem2  35764  filnetlem4  36749  rexrabdioph  43378  fnwe2lem2  43635  fourierdlem70  46749  fourierdlem80  46759  dfclnbgr3  48447  stgr1  48582