Theorem in0 4344

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ∩ cin 4089  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-in 4091  df-nul 4279

This theorem is used by:  0in  4346  csbin  4399  res0  5973  dfpo2  6299  predprc  6341  fresaun  6754  oev2  8535  dju0en  10258  ackbij1lem13  10313  ackbij1lem16  10316  incexclem  16011  bitsinv1  16618  bitsinvp1  16625  sadcadd  16634  sadadd2  16636  sadid1  16644  bitsres  16649  smumullem  16668  ressbas  17420  sylow2a  19839  ablfac1eu  20295  indistopon  23325  fctop  23328  cctop  23330  rest0  23493  filconn  24208  volinun  25873  itg2cnlem2  26089  pthdlem2  30360  0pth  30722  1pthdlem2  30733  disjdifprg  33217  disjun0  33237  ofpreima2  33308  of0r  33321  ldgenpisyslem1  34843  0elcarsg  34986  carsgclctunlem1  34996  carsgclctunlem3  34999  ballotlemfval0  35175  sate0  36267  elima4  36633  bj-rest10  38102  bj-rest0  38107  mblfinlem2  38670  conrel1d  44757  conrel2d  44758  ntrk0kbimka  45133  clsneibex  45196  neicvgbex  45206  qinioo  46641  nnfoctbdjlem  47559  caragen0  47610  resinsnALT  50080