Theorem dfin5 3548

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

Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  {crab 2900   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-rab 2905  df-in 3547

This theorem is referenced by:  nfin  3782  rabbi2dva  3783  dfepfr  5023  epfrc  5024  pmtrmvd  17699  ablfaclem3  18309  mretopd  20706  ptclsg  21228  xkopt  21268  iscmet3  22899  xrlimcnp  24495  ppiub  24729  xppreima  28829  fpwrelmapffs  28897  orvcelval  29857  sstotbnd2  32743  glbconN  33681  2polssN  34219  rfovcnvf1od  37318  fsovcnvlem  37327  ntrneifv3  37400  ntrneifv4  37403  clsneifv3  37428  clsneifv4  37429  neicvgfv  37439