Theorem dfin5 3921

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

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {cab 2747  {crab 3423   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-rab 3424  df-in 3920

This theorem is referenced by:  incom  4170  ineq1  4174  rabbi2dva  4186  dfss7  4212  dfepfr  5643  epfrc  5644  pmtrmvd  19522  ablfaclem3  20155  mretopd  23214  ptclsg  23737  xkopt  23777  iscmet3  25417  xrlimcnp  27095  ppiub  27330  xppreima  32927  fpwrelmapffs  33016  orvcelval  34800  sstotbnd2  38308  glbconN  40036  2polssN  40574  rfovcnvf1od  44615  fsovcnvlem  44624  ntrneifv3  44693  ntrneifv4  44696  clsneifv3  44721  clsneifv4  44722  neicvgfv  44732  inpw  49481