Theorem dfin5 3932

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {cab 2712  {crab 3413   ∩ cin 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-rab 3414  df-in 3931

This theorem is referenced by:  incom  4182  ineq1  4186  nfinOLD  4198  rabbi2dva  4199  dfss7  4224  dfepfr  5635  epfrc  5636  pmtrmvd  19422  ablfaclem3  20055  mretopd  23015  ptclsg  23538  xkopt  23578  iscmet3  25230  xrlimcnp  26914  ppiub  27151  xppreima  32556  fpwrelmapffs  32646  orvcelval  34409  sstotbnd2  37719  glbconN  39316  glbconNOLD  39317  2polssN  39855  rfovcnvf1od  43953  fsovcnvlem  43962  ntrneifv3  44031  ntrneifv4  44034  clsneifv3  44059  clsneifv4  44060  neicvgfv  44070  inpw  48684