Theorem rexeqi 3338

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexrab2  3632  rexprgf  4626  rextpg  4632  rexopabb  5434  rexxp  5740  elidinxpid  5941  elrid  5942  oarec  8355  wwlktovfo  14601  dvdsprmpweqnn  16514  4sqlem12  16585  pmatcollpw3fi1  21845  cmpfi  22467  txbas  22626  xkobval  22645  ustn0  23280  imasdsf1olem  23434  xpsdsval  23442  plyun0  25263  coeeu  25291  1cubr  25897  dfnbgr3  27608  wlkvtxedg  27913  wwlksn0  28129  eucrctshift  28508  adjbdln  30346  elunirnmbfm  32120  satfbrsuc  33228  fmla1  33249  satffunlem2lem2  33268  brttrcl2  33700  ttrcltr  33702  rnttrcl  33708  made0  33984  addsid1  34054  filnetlem4  34497  rexrabdioph  40532  fnwe2lem2  40792  fourierdlem70  43607  fourierdlem80  43617