Theorem in0 4345

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∩ cin 3898  ∅c0 4279

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  0in  4347  csbin  4400  res0  5976  dfpo2  6294  predprc  6336  fresaun  6746  oev2  8510  dju0en  10178  ackbij1lem13  10233  ackbij1lem16  10236  incexclem  15925  bitsinv1  16532  bitsinvp1  16539  sadcadd  16548  sadadd2  16550  sadid1  16558  bitsres  16563  smumullem  16582  ressbas  17328  sylow2a  19746  ablfac1eu  20202  indistopon  23226  fctop  23229  cctop  23231  rest0  23394  filconn  24109  volinun  25774  itg2cnlem2  25990  pthdlem2  30233  0pth  30595  1pthdlem2  30606  disjdifprg  33048  disjun0  33068  ofpreima2  33139  of0r  33152  ldgenpisyslem1  34674  0elcarsg  34818  carsgclctunlem1  34828  carsgclctunlem3  34831  ballotlemfval0  35007  sate0  35994  elima4  36355  bj-rest10  37838  bj-rest0  37843  mblfinlem2  38407  conrel1d  44503  conrel2d  44504  ntrk0kbimka  44879  clsneibex  44942  neicvgbex  44952  qinioo  46365  nnfoctbdjlem  47283  caragen0  47334  resinsnALT  49799