Theorem in0 4111

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 4062	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 1004	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 214	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 3949	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ∩ cin 3714  ∅c0 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-nul 4059

This theorem is referenced by:  0in  4112  csbin  4153  res0  5555  fresaun  6236  oev2  7774  cda0en  9213  ackbij1lem13  9266  ackbij1lem16  9269  incexclem  14787  bitsinv1  15386  bitsinvp1  15393  sadcadd  15402  sadadd2  15404  sadid1  15412  bitsres  15417  smumullem  15436  ressbas  16152  sylow2a  18254  ablfac1eu  18692  indistopon  21027  fctop  21030  cctop  21032  rest0  21195  filconn  21908  volinun  23534  itg2cnlem2  23748  pthdlem2  26895  0pth  27298  1pthdlem2  27309  disjdifprg  29716  disjun0  29736  ofpreima2  29796  ldgenpisyslem1  30556  0elcarsg  30699  carsgclctunlem1  30709  carsgclctunlem3  30712  ballotlemfval0  30887  dfpo2  31973  elima4  32005  bj-rest10  33365  bj-rest0  33370  mblfinlem2  33778  conrel1d  38475  conrel2d  38476  ntrk0kbimka  38857  clsneibex  38920  neicvgbex  38930  qinioo  40283  nnfoctbdjlem  41193  caragen0  41244