Theorem rexeqi 3292

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∃wrex 3057

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-rex 3058

This theorem is referenced by:  rexrab2  3655  rexprgf  4649  rextpg  4653  rexopabb  5473  rexxp  5788  elidinxpid  6000  elrid  6001  oarec  8485  brttrcl2  9613  ttrcltr  9615  rnttrcl  9621  wwlktovfo  14869  dvdsprmpweqnn  16801  4sqlem12  16872  pzriprnglem10  21431  pmatcollpw3fi1  22706  cmpfi  23326  txbas  23485  xkobval  23504  ustn0  24139  imasdsf1olem  24291  xpsdsval  24299  plyun0  26132  coeeu  26160  1cubr  26782  made0  27821  addsrid  27910  muls01  28054  mulsrid  28055  precsexlemcbv  28147  dfnbgr3  29320  wlkvtxedg  29626  wwlksn0  29845  eucrctshift  30227  adjbdln  32067  elunirnmbfm  34288  onvf1odlem2  35171  satfbrsuc  35433  fmla1  35454  satffunlem2lem2  35473  filnetlem4  36448  rexrabdioph  42914  fnwe2lem2  43171  fourierdlem70  46301  fourierdlem80  46311  dfclnbgr3  47953  stgr1  48088