Theorem dfin5 3914

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

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {cab 2741  {crab 3416   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-rab 3417  df-in 3913

This theorem is referenced by:  incom  4163  ineq1  4167  rabbi2dva  4179  dfss7  4205  dfepfr  5647  epfrc  5648  pmtrmvd  19527  ablfaclem3  20160  mretopd  23230  ptclsg  23753  xkopt  23793  iscmet3  25433  xrlimcnp  27114  ppiub  27349  xppreima  32971  fpwrelmapffs  33060  orvcelval  34840  sstotbnd2  38406  glbconN  40132  2polssN  40670  rfovcnvf1od  44713  fsovcnvlem  44722  ntrneifv3  44791  ntrneifv4  44794  clsneifv3  44819  clsneifv4  44820  neicvgfv  44830  inpw  49586