Theorem dfin5 3806

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

Syntax hints:   ∧ wa 386   = wceq 1658   ∈ wcel 2166  {cab 2811  {crab 3121   ∩ cin 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2818  df-rab 3126  df-in 3805

This theorem is referenced by:  nfin  4045  rabbi2dva  4046  dfepfr  5327  epfrc  5328  pmtrmvd  18226  ablfaclem3  18840  mretopd  21267  ptclsg  21789  xkopt  21829  iscmet3  23461  xrlimcnp  25108  ppiub  25342  xppreima  29998  fpwrelmapffs  30057  orvcelval  31076  sstotbnd2  34115  glbconN  35452  2polssN  35990  rfovcnvf1od  39138  fsovcnvlem  39147  ntrneifv3  39220  ntrneifv4  39223  clsneifv3  39248  clsneifv4  39249  neicvgfv  39259  dfss7  42180