Theorem dfin5 3906

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 3905	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
2		df-rab 3397	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	1, 2	eqtr4i 2759	1 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2711  {crab 3396   ∩ cin 3897

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-rab 3397  df-in 3905

This theorem is referenced by:  incom  4158  ineq1  4162  nfinOLD  4174  rabbi2dva  4175  dfss7  4200  dfepfr  5605  epfrc  5606  pmtrmvd  19376  ablfaclem3  20009  mretopd  23027  ptclsg  23550  xkopt  23590  iscmet3  25240  xrlimcnp  26925  ppiub  27162  xppreima  32649  fpwrelmapffs  32741  orvcelval  34554  sstotbnd2  37887  glbconN  39549  2polssN  40087  rfovcnvf1od  44161  fsovcnvlem  44170  ntrneifv3  44239  ntrneifv4  44242  clsneifv3  44267  clsneifv4  44268  neicvgfv  44278  inpw  48986