Theorem in0 4352

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ∩ cin 3905  ∅c0 4286

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-in 3913  df-nul 4287

This theorem is used by:  0in  4354  csbin  4407  res0  5984  dfpo2  6301  predprc  6343  fresaun  6753  oev2  8510  dju0en  10171  ackbij1lem13  10226  ackbij1lem16  10229  incexclem  15908  bitsinv1  16517  bitsinvp1  16524  sadcadd  16533  sadadd2  16535  sadid1  16543  bitsres  16548  smumullem  16567  ressbas  17313  sylow2a  19712  ablfac1eu  20168  indistopon  23187  fctop  23190  cctop  23192  rest0  23355  filconn  24069  volinun  25734  itg2cnlem2  25950  pthdlem2  30146  0pth  30505  1pthdlem2  30516  disjdifprg  32949  disjun0  32969  ofpreima2  33040  of0r  33053  ldgenpisyslem1  34577  0elcarsg  34721  carsgclctunlem1  34731  carsgclctunlem3  34734  ballotlemfval0  34910  sate0  35920  elima4  36281  bj-rest10  37763  bj-rest0  37768  mblfinlem2  38342  conrel1d  44422  conrel2d  44423  ntrk0kbimka  44798  clsneibex  44861  neicvgbex  44871  qinioo  46284  nnfoctbdjlem  47202  caragen0  47253  resinsnALT  49684