Theorem rexeqi 3416

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

Syntax hints:   ↔ wb 208   = wceq 1537  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-rex 3146

This theorem is referenced by:  rexrab2  3695  rexprgf  4633  rextpg  4637  rexopabb  5417  rexxp  5715  elidinxpid  5914  elrid  5915  oarec  8190  wwlktovfo  14324  dvdsprmpweqnn  16223  4sqlem12  16294  pmatcollpw3fi1  21398  cmpfi  22018  txbas  22177  xkobval  22196  ustn0  22831  imasdsf1olem  22985  xpsdsval  22993  plyun0  24789  coeeu  24817  1cubr  25422  dfnbgr3  27122  wlkvtxedg  27427  wwlksn0  27643  eucrctshift  28024  adjbdln  29862  elunirnmbfm  31513  satfbrsuc  32615  fmla1  32636  satffunlem2lem2  32655  filnetlem4  33731  rexrabdioph  39398  fnwe2lem2  39658  fourierdlem70  42468  fourierdlem80  42478