Theorem rexeqi 3297

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

Syntax hints:   ↔ wb 207   = wceq 1547  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-rex 3065

This theorem is referenced by:  rexrab2  3648  rexprgf  4634  rextpg  4638  rexopabb  5477  rexxp  5791  elidinxpid  6004  elrid  6005  oarec  8494  brttrcl2  9633  ttrcltr  9635  rnttrcl  9641  wwlktovfo  14918  dvdsprmpweqnn  16854  4sqlem12  16925  pzriprnglem10  21472  pmatcollpw3fi1  22778  cmpfi  23398  txbas  23557  xkobval  23576  ustn0  24211  imasdsf1olem  24363  xpsdsval  24371  plyun0  26187  coeeu  26215  1cubr  26831  made0  27880  addsrid  27981  muls01  28129  mulsrid  28130  precsexlemcbv  28223  dfnbgr3  29432  wlkvtxedg  29737  wwlksn0  29956  eucrctshift  30338  adjbdln  32179  elunirnmbfm  34443  onvf1odlem2  35339  satfbrsuc  35601  fmla1  35622  satffunlem2lem2  35641  filnetlem4  36616  rexrabdioph  43246  fnwe2lem2  43503  fourierdlem70  46626  fourierdlem80  46636  dfclnbgr3  48324  stgr1  48459