Theorem dfin5 3919

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  {crab 3402   ∩ cin 3910

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-rab 3403  df-in 3918

This theorem is referenced by:  incom  4168  ineq1  4172  nfinOLD  4184  rabbi2dva  4185  dfss7  4210  dfepfr  5615  epfrc  5616  pmtrmvd  19362  ablfaclem3  19995  mretopd  22955  ptclsg  23478  xkopt  23518  iscmet3  25169  xrlimcnp  26854  ppiub  27091  xppreima  32542  fpwrelmapffs  32630  orvcelval  34433  sstotbnd2  37741  glbconN  39343  glbconNOLD  39344  2polssN  39882  rfovcnvf1od  43966  fsovcnvlem  43975  ntrneifv3  44044  ntrneifv4  44047  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  inpw  48786