Theorem dfin5 3891

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {cab 2715  {crab 3067   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-rab 3072  df-in 3890

This theorem is referenced by:  incom  4131  ineq1  4136  nfin  4147  rabbi2dva  4148  dfss7  4171  dfepfr  5565  epfrc  5566  pmtrmvd  18979  ablfaclem3  19605  mretopd  22151  ptclsg  22674  xkopt  22714  iscmet3  24362  xrlimcnp  26023  ppiub  26257  xppreima  30884  fpwrelmapffs  30971  orvcelval  32335  sstotbnd2  35859  glbconN  37318  2polssN  37856  rfovcnvf1od  41501  fsovcnvlem  41510  ntrneifv3  41581  ntrneifv4  41584  clsneifv3  41609  clsneifv4  41610  neicvgfv  41620  inpw  46052