Theorem dfin5 3889

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

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  {crab 3110   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-rab 3115  df-in 3888

This theorem is referenced by:  incom  4128  ineq1  4131  nfin  4143  rabbi2dva  4144  dfss7  4167  dfepfr  5504  epfrc  5505  pmtrmvd  18576  ablfaclem3  19202  mretopd  21697  ptclsg  22220  xkopt  22260  iscmet3  23897  xrlimcnp  25554  ppiub  25788  xppreima  30408  fpwrelmapffs  30496  orvcelval  31836  sstotbnd2  35212  glbconN  36673  2polssN  37211  rfovcnvf1od  40705  fsovcnvlem  40714  ntrneifv3  40785  ntrneifv4  40788  clsneifv3  40813  clsneifv4  40814  neicvgfv  40824