Theorem dfin5 3907

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2739  {crab 3413   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-rab 3414  df-in 3906

This theorem is used by:  incom  4155  ineq1  4159  rabbi2dva  4171  dfss7  4197  dfepfr  5635  epfrc  5636  pmtrmvd  19663  ablfaclem3  20296  mretopd  23403  ptclsg  23927  xkopt  23967  iscmet3  25607  xrlimcnp  27289  ppiub  27524  xppreima  33232  fpwrelmapffs  33319  orvcelval  35094  sstotbnd2  38688  glbconN  40414  2polssN  40952  rfovcnvf1od  44989  fsovcnvlem  44998  ntrneifv3  45067  ntrneifv4  45070  clsneifv3  45095  clsneifv4  45096  neicvgfv  45106  inpw  49904