Theorem dfin5 3723

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

Syntax hints:   ∧ wa 383   = wceq 1632   ∈ wcel 2139  {cab 2746  {crab 3054   ∩ cin 3714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-rab 3059  df-in 3722

This theorem is referenced by:  nfin  3963  rabbi2dva  3964  dfepfr  5251  epfrc  5252  pmtrmvd  18076  ablfaclem3  18686  mretopd  21098  ptclsg  21620  xkopt  21660  iscmet3  23291  xrlimcnp  24894  ppiub  25128  xppreima  29758  fpwrelmapffs  29818  orvcelval  30839  sstotbnd2  33886  glbconN  35166  2polssN  35704  rfovcnvf1od  38800  fsovcnvlem  38809  ntrneifv3  38882  ntrneifv4  38885  clsneifv3  38910  clsneifv4  38911  neicvgfv  38921