Theorem rexeqi 3295

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

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

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 2708

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

This theorem is referenced by:  rexrab2  3658  rexprgf  4652  rextpg  4656  rexopabb  5476  rexxp  5791  elidinxpid  6004  elrid  6005  oarec  8489  brttrcl2  9623  ttrcltr  9625  rnttrcl  9631  wwlktovfo  14881  dvdsprmpweqnn  16813  4sqlem12  16884  pzriprnglem10  21445  pmatcollpw3fi1  22732  cmpfi  23352  txbas  23511  xkobval  23530  ustn0  24165  imasdsf1olem  24317  xpsdsval  24325  plyun0  26158  coeeu  26186  1cubr  26808  made0  27859  addsrid  27960  muls01  28108  mulsrid  28109  precsexlemcbv  28202  dfnbgr3  29411  wlkvtxedg  29717  wwlksn0  29936  eucrctshift  30318  adjbdln  32158  elunirnmbfm  34409  onvf1odlem2  35298  satfbrsuc  35560  fmla1  35581  satffunlem2lem2  35600  filnetlem4  36575  rexrabdioph  43036  fnwe2lem2  43293  fourierdlem70  46420  fourierdlem80  46430  dfclnbgr3  48072  stgr1  48207