Theorem dfin5 3910

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

Syntax hints:   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {cab 2739  {crab 3413   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-rab 3414  df-in 3909

This theorem is referenced by:  incom  4159  ineq1  4163  rabbi2dva  4175  dfss7  4201  dfepfr  5627  epfrc  5628  pmtrmvd  19487  ablfaclem3  20120  mretopd  23140  ptclsg  23663  xkopt  23703  iscmet3  25343  xrlimcnp  27021  ppiub  27256  xppreima  32808  fpwrelmapffs  32897  orvcelval  34727  sstotbnd2  38234  glbconN  39962  2polssN  40500  rfovcnvf1od  44541  fsovcnvlem  44550  ntrneifv3  44619  ntrneifv4  44622  clsneifv3  44647  clsneifv4  44648  neicvgfv  44658  inpw  49407