Theorem dfin5 3944

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {cab 2799  {crab 3142   ∩ cin 3935

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-rab 3147  df-in 3943

This theorem is referenced by:  incom  4178  ineq1  4181  nfin  4193  rabbi2dva  4194  dfss7  4217  dfepfr  5540  epfrc  5541  pmtrmvd  18584  ablfaclem3  19209  mretopd  21700  ptclsg  22223  xkopt  22263  iscmet3  23896  xrlimcnp  25546  ppiub  25780  xppreima  30394  fpwrelmapffs  30470  orvcelval  31726  sstotbnd2  35067  glbconN  36528  2polssN  37066  rfovcnvf1od  40370  fsovcnvlem  40379  ntrneifv3  40452  ntrneifv4  40455  clsneifv3  40480  clsneifv4  40481  neicvgfv  40491