Theorem dfin5 4091

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  {crab 3412   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-rab 3413  df-in 4090

This theorem is used by:  incom  4105  ineq1  4109  rabbi2dva  4121  dfss7  4147  dfepfr  5634  epfrc  5635  pmtrmvd  19677  ablfaclem3  20310  mretopd  23417  ptclsg  23941  xkopt  23981  iscmet3  25621  xrlimcnp  27303  ppiub  27538  xppreima  33288  fpwrelmapffs  33374  orvcelval  35149  sstotbnd2  38815  glbconN  40541  2polssN  41079  rfovcnvf1od  45111  fsovcnvlem  45120  ntrneifv3  45189  ntrneifv4  45192  clsneifv3  45217  clsneifv4  45218  neicvgfv  45228  inpw  50043