Theorem dfin5 3582

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

Syntax hints:   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {cab 2608  {crab 2916   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-rab 2921  df-in 3581

This theorem is referenced by:  nfin  3820  rabbi2dva  3821  dfepfr  5099  epfrc  5100  pmtrmvd  17876  ablfaclem3  18486  mretopd  20896  ptclsg  21418  xkopt  21458  iscmet3  23091  xrlimcnp  24695  ppiub  24929  xppreima  29449  fpwrelmapffs  29509  orvcelval  30530  sstotbnd2  33573  glbconN  34663  2polssN  35201  rfovcnvf1od  38298  fsovcnvlem  38307  ntrneifv3  38380  ntrneifv4  38383  clsneifv3  38408  clsneifv4  38409  neicvgfv  38419