Theorem in0 4344

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 4287	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 533	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4161	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∩ cin 3897  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-in 3905  df-nul 4283

This theorem is referenced by:  0in  4346  csbin  4391  res0  5939  dfpo2  6251  predprc  6293  fresaun  6702  oev2  8447  dju0en  10078  ackbij1lem13  10133  ackbij1lem16  10136  incexclem  15750  bitsinv1  16360  bitsinvp1  16367  sadcadd  16376  sadadd2  16378  sadid1  16386  bitsres  16391  smumullem  16410  ressbas  17154  sylow2a  19539  ablfac1eu  19995  indistopon  22936  fctop  22939  cctop  22941  rest0  23104  filconn  23818  volinun  25494  itg2cnlem2  25710  pthdlem2  29767  0pth  30126  1pthdlem2  30137  disjdifprg  32576  disjun0  32596  ofpreima2  32670  of0r  32684  ldgenpisyslem1  34248  0elcarsg  34392  carsgclctunlem1  34402  carsgclctunlem3  34405  ballotlemfval0  34581  sate0  35531  elima4  35892  bj-rest10  37205  bj-rest0  37210  mblfinlem2  37771  conrel1d  43820  conrel2d  43821  ntrk0kbimka  44196  clsneibex  44259  neicvgbex  44269  qinioo  45697  nnfoctbdjlem  46615  caragen0  46666  resinsnALT  49034