Theorem dfin5 3907

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2738  {crab 3412   ∩ cin 3898

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-rab 3413  df-in 3906

This theorem is used by:  incom  4155  ineq1  4159  rabbi2dva  4171  dfss7  4197  dfepfr  5639  epfrc  5640  pmtrmvd  19583  ablfaclem3  20216  mretopd  23317  ptclsg  23841  xkopt  23881  iscmet3  25521  xrlimcnp  27205  ppiub  27440  xppreima  33118  fpwrelmapffs  33205  orvcelval  34980  sstotbnd2  38524  glbconN  40250  2polssN  40788  rfovcnvf1od  44844  fsovcnvlem  44853  ntrneifv3  44922  ntrneifv4  44925  clsneifv3  44950  clsneifv4  44951  neicvgfv  44961  inpw  49753