Theorem rexeqi 3329

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

Syntax hints:   ↔ wb 209   = wceq 1539  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-clel 2831  df-rex 3077

This theorem is referenced by:  rexrab2  3617  rexprgf  4589  rextpg  4593  rexopabb  5386  rexxp  5683  elidinxpid  5885  elrid  5886  oarec  8199  wwlktovfo  14370  dvdsprmpweqnn  16277  4sqlem12  16348  pmatcollpw3fi1  21489  cmpfi  22109  txbas  22268  xkobval  22287  ustn0  22922  imasdsf1olem  23076  xpsdsval  23084  plyun0  24894  coeeu  24922  1cubr  25528  dfnbgr3  27228  wlkvtxedg  27533  wwlksn0  27749  eucrctshift  28128  adjbdln  29966  elunirnmbfm  31740  satfbrsuc  32845  fmla1  32866  satffunlem2lem2  32885  made0  33615  addsid1  33676  filnetlem4  34120  rexrabdioph  40109  fnwe2lem2  40369  fourierdlem70  43185  fourierdlem80  43195