Theorem dfin5 3897

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2714  {crab 3389   ∩ cin 3888

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-rab 3390  df-in 3896

This theorem is referenced by:  incom  4149  ineq1  4153  nfinOLD  4165  rabbi2dva  4166  dfss7  4191  dfepfr  5615  epfrc  5616  pmtrmvd  19431  ablfaclem3  20064  mretopd  23057  ptclsg  23580  xkopt  23620  iscmet3  25260  xrlimcnp  26932  ppiub  27167  xppreima  32718  fpwrelmapffs  32807  orvcelval  34613  sstotbnd2  38095  glbconN  39823  2polssN  40361  rfovcnvf1od  44431  fsovcnvlem  44440  ntrneifv3  44509  ntrneifv4  44512  clsneifv3  44537  clsneifv4  44538  neicvgfv  44548  inpw  49300