Theorem dfin5 3909

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  {crab 3399   ∩ cin 3900

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-rab 3400  df-in 3908

This theorem is referenced by:  incom  4161  ineq1  4165  nfinOLD  4177  rabbi2dva  4178  dfss7  4203  dfepfr  5608  epfrc  5609  pmtrmvd  19385  ablfaclem3  20018  mretopd  23036  ptclsg  23559  xkopt  23599  iscmet3  25249  xrlimcnp  26934  ppiub  27171  xppreima  32723  fpwrelmapffs  32813  orvcelval  34626  sstotbnd2  37975  glbconN  39637  2polssN  40175  rfovcnvf1od  44245  fsovcnvlem  44254  ntrneifv3  44323  ntrneifv4  44326  clsneifv3  44351  clsneifv4  44352  neicvgfv  44362  inpw  49070