Theorem dfin5 3891

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

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2717  {crab 3391   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-rab 3392  df-in 3890

This theorem is referenced by:  incom  4138  ineq1  4142  rabbi2dva  4154  dfss7  4179  dfepfr  5602  epfrc  5603  pmtrmvd  19422  ablfaclem3  20055  mretopd  23075  ptclsg  23598  xkopt  23638  iscmet3  25278  xrlimcnp  26950  ppiub  27185  xppreima  32737  fpwrelmapffs  32826  orvcelval  34653  sstotbnd2  38141  glbconN  39869  2polssN  40407  rfovcnvf1od  44448  fsovcnvlem  44457  ntrneifv3  44526  ntrneifv4  44529  clsneifv3  44554  clsneifv4  44555  neicvgfv  44565  inpw  49315