Theorem in0 4346

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 4288	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 541	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 226	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4162	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ∩ cin 3901  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-in 3909  df-nul 4284

This theorem is referenced by:  0in  4348  csbin  4393  res0  5965  dfpo2  6278  predprc  6320  fresaun  6730  oev2  8486  dju0en  10126  ackbij1lem13  10181  ackbij1lem16  10184  incexclem  15857  bitsinv1  16467  bitsinvp1  16474  sadcadd  16483  sadadd2  16485  sadid1  16493  bitsres  16498  smumullem  16517  ressbas  17263  sylow2a  19650  ablfac1eu  20106  indistopon  23049  fctop  23052  cctop  23054  rest0  23217  filconn  23931  volinun  25596  itg2cnlem2  25812  pthdlem2  29925  0pth  30284  1pthdlem2  30295  disjdifprg  32735  disjun0  32755  ofpreima2  32829  of0r  32842  ldgenpisyslem1  34421  0elcarsg  34565  carsgclctunlem1  34575  carsgclctunlem3  34578  ballotlemfval0  34754  sate0  35726  elima4  36087  bj-rest10  37539  bj-rest0  37544  mblfinlem2  38118  conrel1d  44200  conrel2d  44201  ntrk0kbimka  44576  clsneibex  44639  neicvgbex  44649  qinioo  46072  nnfoctbdjlem  46990  caragen0  47041  resinsnALT  49455