Theorem dfin5 3952

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2708  {crab 3431   ∩ cin 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-rab 3432  df-in 3951

This theorem is referenced by:  incom  4197  ineq1  4201  nfin  4212  rabbi2dva  4213  dfss7  4236  dfepfr  5654  epfrc  5655  pmtrmvd  19288  ablfaclem3  19916  mretopd  22525  ptclsg  23048  xkopt  23088  iscmet3  24739  xrlimcnp  26400  ppiub  26634  xppreima  31740  fpwrelmapffs  31830  orvcelval  33298  sstotbnd2  36447  glbconN  38052  glbconNOLD  38053  2polssN  38591  rfovcnvf1od  42526  fsovcnvlem  42535  ntrneifv3  42604  ntrneifv4  42607  clsneifv3  42632  clsneifv4  42633  neicvgfv  42643  inpw  47151