Theorem dfin5 3893

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

Syntax hints:   ∧ wa 397   = wceq 1548   ∈ wcel 2121  {cab 2719  {crab 3393   ∩ cin 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-rab 3394  df-in 3892

This theorem is referenced by:  incom  4141  ineq1  4145  rabbi2dva  4157  dfss7  4182  dfepfr  5605  epfrc  5606  pmtrmvd  19426  ablfaclem3  20059  mretopd  23079  ptclsg  23602  xkopt  23642  iscmet3  25282  xrlimcnp  26954  ppiub  27189  xppreima  32741  fpwrelmapffs  32830  orvcelval  34665  sstotbnd2  38156  glbconN  39884  2polssN  40422  rfovcnvf1od  44463  fsovcnvlem  44472  ntrneifv3  44541  ntrneifv4  44544  clsneifv3  44569  clsneifv4  44570  neicvgfv  44580  inpw  49329