Theorem dfin5 3934

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2713  {crab 3415   ∩ cin 3925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-rab 3416  df-in 3933

This theorem is referenced by:  incom  4184  ineq1  4188  nfinOLD  4200  rabbi2dva  4201  dfss7  4226  dfepfr  5638  epfrc  5639  pmtrmvd  19437  ablfaclem3  20070  mretopd  23030  ptclsg  23553  xkopt  23593  iscmet3  25245  xrlimcnp  26930  ppiub  27167  xppreima  32623  fpwrelmapffs  32711  orvcelval  34501  sstotbnd2  37798  glbconN  39395  glbconNOLD  39396  2polssN  39934  rfovcnvf1od  44028  fsovcnvlem  44037  ntrneifv3  44106  ntrneifv4  44109  clsneifv3  44134  clsneifv4  44135  neicvgfv  44145  inpw  48803