Theorem dfin5 3547

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

Syntax hints:   ∧ wa 382   = wceq 1474   ∈ wcel 1976  {cab 2595  {crab 2899   ∩ cin 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-rab 2904  df-in 3546

This theorem is referenced by:  nfin  3781  rabbi2dva  3782  dfepfr  5013  epfrc  5014  pmtrmvd  17645  ablfaclem3  18255  mretopd  20648  ptclsg  21170  xkopt  21210  iscmet3  22817  xrlimcnp  24412  ppiub  24646  xppreima  28635  fpwrelmapffs  28703  orvcelval  29663  sstotbnd2  32539  glbconN  33477  2polssN  34015  rfovcnvf1od  37114  fsovcnvlem  37123  ntrneifv3  37196  ntrneifv4  37199  clsneifv3  37224  clsneifv4  37225  neicvgfv  37235