Theorem dfin5 4095

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {cab 2741  {crab 3416   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-rab 3417  df-in 4094

This theorem is used by:  incom  4109  ineq1  4113  rabbi2dva  4125  dfss7  4151  dfepfr  5642  epfrc  5643  pmtrmvd  19721  ablfaclem3  20354  mretopd  23465  ptclsg  23989  xkopt  24029  iscmet3  25669  xrlimcnp  27353  ppiub  27588  xppreima  33337  fpwrelmapffs  33422  orvcelval  35212  sstotbnd2  38974  glbconN  40700  2polssN  41238  rfovcnvf1od  45265  fsovcnvlem  45274  ntrneifv3  45343  ntrneifv4  45346  clsneifv3  45371  clsneifv4  45372  neicvgfv  45382  inpw  50267