Theorem in0 4348

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∩ cin 3904  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-in 3912  df-nul 4287

This theorem is referenced by:  0in  4350  csbin  4395  res0  5938  dfpo2  6248  predprc  6290  fresaun  6699  oev2  8448  dju0en  10089  ackbij1lem13  10144  ackbij1lem16  10147  incexclem  15761  bitsinv1  16371  bitsinvp1  16378  sadcadd  16387  sadadd2  16389  sadid1  16397  bitsres  16402  smumullem  16421  ressbas  17165  sylow2a  19516  ablfac1eu  19972  indistopon  22904  fctop  22907  cctop  22909  rest0  23072  filconn  23786  volinun  25463  itg2cnlem2  25679  pthdlem2  29731  0pth  30087  1pthdlem2  30098  disjdifprg  32537  disjun0  32557  ofpreima2  32623  of0r  32635  ldgenpisyslem1  34132  0elcarsg  34277  carsgclctunlem1  34287  carsgclctunlem3  34290  ballotlemfval0  34466  sate0  35390  elima4  35751  bj-rest10  37064  bj-rest0  37069  mblfinlem2  37640  conrel1d  43639  conrel2d  43640  ntrk0kbimka  44015  clsneibex  44078  neicvgbex  44088  qinioo  45520  nnfoctbdjlem  46440  caragen0  46491  resinsnALT  48861