Theorem in0 4349

Description: The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
in0	⊢ (𝐴 ∩ ∅) = ∅

Proof of Theorem in0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4292	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 533	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4166	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∩ cin 3902  ∅c0 4287

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-in 3910  df-nul 4288

This theorem is referenced by:  0in  4351  csbin  4396  res0  5950  dfpo2  6262  predprc  6304  fresaun  6713  oev2  8460  dju0en  10098  ackbij1lem13  10153  ackbij1lem16  10156  incexclem  15771  bitsinv1  16381  bitsinvp1  16388  sadcadd  16397  sadadd2  16399  sadid1  16407  bitsres  16412  smumullem  16431  ressbas  17175  sylow2a  19560  ablfac1eu  20016  indistopon  22957  fctop  22960  cctop  22962  rest0  23125  filconn  23839  volinun  25515  itg2cnlem2  25731  pthdlem2  29853  0pth  30212  1pthdlem2  30223  disjdifprg  32661  disjun0  32681  ofpreima2  32755  of0r  32768  ldgenpisyslem1  34340  0elcarsg  34484  carsgclctunlem1  34494  carsgclctunlem3  34497  ballotlemfval0  34673  sate0  35628  elima4  35989  bj-rest10  37338  bj-rest0  37343  mblfinlem2  37906  conrel1d  44016  conrel2d  44017  ntrk0kbimka  44392  clsneibex  44455  neicvgbex  44465  qinioo  45892  nnfoctbdjlem  46810  caragen0  46861  resinsnALT  49229