Theorem dfin5 3943

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

Syntax hints:   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {cab 2799  {crab 3142   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-rab 3147  df-in 3942

This theorem is referenced by:  incom  4177  ineq1  4180  nfin  4192  rabbi2dva  4193  dfss7  4216  dfepfr  5534  epfrc  5535  pmtrmvd  18578  ablfaclem3  19203  mretopd  21694  ptclsg  22217  xkopt  22257  iscmet3  23890  xrlimcnp  25540  ppiub  25774  xppreima  30388  fpwrelmapffs  30464  orvcelval  31721  sstotbnd2  35046  glbconN  36507  2polssN  37045  rfovcnvf1od  40343  fsovcnvlem  40352  ntrneifv3  40425  ntrneifv4  40428  clsneifv3  40453  clsneifv4  40454  neicvgfv  40464