Theorem dfin5 3911

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  {crab 3401   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-rab 3402  df-in 3910

This theorem is referenced by:  incom  4163  ineq1  4167  nfinOLD  4179  rabbi2dva  4180  dfss7  4205  dfepfr  5616  epfrc  5617  pmtrmvd  19397  ablfaclem3  20030  mretopd  23048  ptclsg  23571  xkopt  23611  iscmet3  25261  xrlimcnp  26946  ppiub  27183  xppreima  32734  fpwrelmapffs  32823  orvcelval  34646  sstotbnd2  38022  glbconN  39750  2polssN  40288  rfovcnvf1od  44357  fsovcnvlem  44366  ntrneifv3  44435  ntrneifv4  44438  clsneifv3  44463  clsneifv4  44464  neicvgfv  44474  inpw  49181