Theorem dfin5 3895

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

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {cab 2715  {crab 3068   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-rab 3073  df-in 3894

This theorem is referenced by:  incom  4135  ineq1  4139  nfin  4150  rabbi2dva  4151  dfss7  4174  dfepfr  5574  epfrc  5575  pmtrmvd  19064  ablfaclem3  19690  mretopd  22243  ptclsg  22766  xkopt  22806  iscmet3  24457  xrlimcnp  26118  ppiub  26352  xppreima  30983  fpwrelmapffs  31069  orvcelval  32435  sstotbnd2  35932  glbconN  37391  2polssN  37929  rfovcnvf1od  41612  fsovcnvlem  41621  ntrneifv3  41692  ntrneifv4  41695  clsneifv3  41720  clsneifv4  41721  neicvgfv  41731  inpw  46164