Theorem in0 4340

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ∩ cin 3896  ∅c0 4278

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-in 3904  df-nul 4279

This theorem is referenced by:  0in  4342  csbin  4387  res0  5927  dfpo2  6238  predprc  6280  fresaun  6689  oev2  8433  dju0en  10062  ackbij1lem13  10117  ackbij1lem16  10120  incexclem  15738  bitsinv1  16348  bitsinvp1  16355  sadcadd  16364  sadadd2  16366  sadid1  16374  bitsres  16379  smumullem  16398  ressbas  17142  sylow2a  19526  ablfac1eu  19982  indistopon  22911  fctop  22914  cctop  22916  rest0  23079  filconn  23793  volinun  25469  itg2cnlem2  25685  pthdlem2  29741  0pth  30097  1pthdlem2  30108  disjdifprg  32547  disjun0  32567  ofpreima2  32640  of0r  32652  ldgenpisyslem1  34168  0elcarsg  34312  carsgclctunlem1  34322  carsgclctunlem3  34325  ballotlemfval0  34501  sate0  35451  elima4  35812  bj-rest10  37122  bj-rest0  37127  mblfinlem2  37698  conrel1d  43696  conrel2d  43697  ntrk0kbimka  44072  clsneibex  44135  neicvgbex  44145  qinioo  45575  nnfoctbdjlem  46493  caragen0  46544  resinsnALT  48904