Theorem dfin5 3905

Description: Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)

Assertion

Ref	Expression
dfin5	⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfin5

Step	Hyp	Ref	Expression
1		df-in 3904	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
2		df-rab 3396	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	1, 2	eqtr4i 2757	1 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {cab 2709  {crab 3395   ∩ cin 3896

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-rab 3396  df-in 3904

This theorem is referenced by:  incom  4154  ineq1  4158  nfinOLD  4170  rabbi2dva  4171  dfss7  4196  dfepfr  5595  epfrc  5596  pmtrmvd  19363  ablfaclem3  19996  mretopd  23002  ptclsg  23525  xkopt  23565  iscmet3  25215  xrlimcnp  26900  ppiub  27137  xppreima  32619  fpwrelmapffs  32709  orvcelval  34474  sstotbnd2  37814  glbconN  39416  2polssN  39954  rfovcnvf1od  44037  fsovcnvlem  44046  ntrneifv3  44115  ntrneifv4  44118  clsneifv3  44143  clsneifv4  44144  neicvgfv  44154  inpw  48856