Theorem dfin5 3957

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

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  {crab 3433   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-rab 3434  df-in 3956

This theorem is referenced by:  incom  4202  ineq1  4206  nfin  4217  rabbi2dva  4218  dfss7  4241  dfepfr  5662  epfrc  5663  pmtrmvd  19324  ablfaclem3  19957  mretopd  22596  ptclsg  23119  xkopt  23159  iscmet3  24810  xrlimcnp  26473  ppiub  26707  xppreima  31871  fpwrelmapffs  31959  orvcelval  33467  sstotbnd2  36642  glbconN  38247  glbconNOLD  38248  2polssN  38786  rfovcnvf1od  42755  fsovcnvlem  42764  ntrneifv3  42833  ntrneifv4  42836  clsneifv3  42861  clsneifv4  42862  neicvgfv  42872  inpw  47503