Theorem rexeqi 3348

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

Syntax hints:   ↔ wb 205   = wceq 1539  ∃wrex 3066

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ral 3070  df-rex 3071

This theorem is referenced by:  rexrab2  3638  rexprgf  4630  rextpg  4636  rexopabb  5442  rexxp  5754  elidinxpid  5955  elrid  5956  oarec  8402  brttrcl2  9481  ttrcltr  9483  rnttrcl  9489  wwlktovfo  14682  dvdsprmpweqnn  16595  4sqlem12  16666  pmatcollpw3fi1  21946  cmpfi  22568  txbas  22727  xkobval  22746  ustn0  23381  imasdsf1olem  23535  xpsdsval  23543  plyun0  25367  coeeu  25395  1cubr  26001  dfnbgr3  27714  wlkvtxedg  28020  wwlksn0  28237  eucrctshift  28616  adjbdln  30454  elunirnmbfm  32229  satfbrsuc  33337  fmla1  33358  satffunlem2lem2  33377  made0  34066  addsid1  34136  filnetlem4  34579  rexrabdioph  40623  fnwe2lem2  40883  fourierdlem70  43724  fourierdlem80  43734