Theorem dfin5 3898

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  {crab 3390   ∩ cin 3889

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-rab 3391  df-in 3897

This theorem is referenced by:  incom  4150  ineq1  4154  nfinOLD  4166  rabbi2dva  4167  dfss7  4192  dfepfr  5608  epfrc  5609  pmtrmvd  19422  ablfaclem3  20055  mretopd  23067  ptclsg  23590  xkopt  23630  iscmet3  25270  xrlimcnp  26945  ppiub  27181  xppreima  32733  fpwrelmapffs  32822  orvcelval  34629  sstotbnd2  38109  glbconN  39837  2polssN  40375  rfovcnvf1od  44449  fsovcnvlem  44458  ntrneifv3  44527  ntrneifv4  44530  clsneifv3  44555  clsneifv4  44556  neicvgfv  44566  inpw  49312