Theorem in0 4348

Description: The intersection of a class with the empty set is the empty set. Dual of unv 4352. Commuted form of in0 4348. 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 4286	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 543	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4112	1 ⊢ (𝐴 ∩ ∅) = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ∩ cin 4092  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-in 4094  df-nul 4282

This theorem is used by:  0in  4350  csbin  4403  res0  5990  dfpo2  6325  predprc  6367  fresaun  6783  oev2  8569  dju0en  10293  ackbij1lem13  10348  ackbij1lem16  10351  incexclem  16049  bitsinv1  16656  bitsinvp1  16663  sadcadd  16672  sadadd2  16674  sadid1  16682  bitsres  16687  smumullem  16706  ressbas  17458  sylow2a  19884  ablfac1eu  20340  indistopon  23374  fctop  23377  cctop  23379  rest0  23542  filconn  24257  volinun  25922  itg2cnlem2  26138  pthdlem2  30411  0pth  30773  1pthdlem2  30784  disjdifprg  33267  disjun0  33287  ofpreima2  33358  of0r  33370  ldgenpisyslem1  34907  0elcarsg  35050  carsgclctunlem1  35060  carsgclctunlem3  35063  ballotlemfval0  35239  sate0  36388  elima4  36755  bj-rest10  38279  bj-rest0  38284  mblfinlem2  38844  conrel1d  44924  conrel2d  44925  ntrk0kbimka  45300  clsneibex  45363  neicvgbex  45373  qinioo  46820  nnfoctbdjlem  47738  caragen0  47789  resinsnALT  50317