Theorem rexeqi 3291

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  rexrab2  3659  rexprgf  4648  rextpg  4652  rexopabb  5468  rexxp  5782  elidinxpid  5994  elrid  5995  oarec  8477  brttrcl2  9604  ttrcltr  9606  rnttrcl  9612  wwlktovfo  14865  dvdsprmpweqnn  16797  4sqlem12  16868  pzriprnglem10  21428  pmatcollpw3fi1  22704  cmpfi  23324  txbas  23483  xkobval  23502  ustn0  24137  imasdsf1olem  24289  xpsdsval  24297  plyun0  26130  coeeu  26158  1cubr  26780  made0  27819  addsrid  27908  muls01  28052  mulsrid  28053  precsexlemcbv  28145  dfnbgr3  29317  wlkvtxedg  29623  wwlksn0  29842  eucrctshift  30221  adjbdln  32061  elunirnmbfm  34263  onvf1odlem2  35146  satfbrsuc  35408  fmla1  35429  satffunlem2lem2  35448  filnetlem4  36421  rexrabdioph  42833  fnwe2lem2  43090  fourierdlem70  46220  fourierdlem80  46230  dfclnbgr3  47863  stgr1  47998