Theorem dfin5 3959

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2714  {crab 3436   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-rab 3437  df-in 3958

This theorem is referenced by:  incom  4209  ineq1  4213  nfinOLD  4225  rabbi2dva  4226  dfss7  4251  dfepfr  5669  epfrc  5670  pmtrmvd  19474  ablfaclem3  20107  mretopd  23100  ptclsg  23623  xkopt  23663  iscmet3  25327  xrlimcnp  27011  ppiub  27248  xppreima  32655  fpwrelmapffs  32745  orvcelval  34471  sstotbnd2  37781  glbconN  39378  glbconNOLD  39379  2polssN  39917  rfovcnvf1od  44017  fsovcnvlem  44026  ntrneifv3  44095  ntrneifv4  44098  clsneifv3  44123  clsneifv4  44124  neicvgfv  44134  inpw  48738