Theorem dfin5 3914

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {cab 2743  {crab 3418   ∩ cin 3905

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-rab 3419  df-in 3913

This theorem is used by:  incom  4162  ineq1  4166  rabbi2dva  4178  dfss7  4204  dfepfr  5647  epfrc  5648  pmtrmvd  19550  ablfaclem3  20183  mretopd  23279  ptclsg  23803  xkopt  23843  iscmet3  25483  xrlimcnp  27164  ppiub  27399  xppreima  33037  fpwrelmapffs  33125  orvcelval  34900  sstotbnd2  38458  glbconN  40184  2polssN  40722  rfovcnvf1od  44763  fsovcnvlem  44772  ntrneifv3  44841  ntrneifv4  44844  clsneifv3  44869  clsneifv4  44870  neicvgfv  44880  inpw  49636