Theorem dfin5 3925

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2708  {crab 3408   ∩ cin 3916

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-rab 3409  df-in 3924

This theorem is referenced by:  incom  4175  ineq1  4179  nfinOLD  4191  rabbi2dva  4192  dfss7  4217  dfepfr  5625  epfrc  5626  pmtrmvd  19393  ablfaclem3  20026  mretopd  22986  ptclsg  23509  xkopt  23549  iscmet3  25200  xrlimcnp  26885  ppiub  27122  xppreima  32576  fpwrelmapffs  32664  orvcelval  34467  sstotbnd2  37775  glbconN  39377  glbconNOLD  39378  2polssN  39916  rfovcnvf1od  44000  fsovcnvlem  44009  ntrneifv3  44078  ntrneifv4  44081  clsneifv3  44106  clsneifv4  44107  neicvgfv  44117  inpw  48817