Theorem in0 4323

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 4266	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 538	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 225	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4141	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ∩ cin 3882  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-in 3890  df-nul 4262

This theorem is referenced by:  0in  4325  csbin  4370  res0  5935  dfpo2  6247  predprc  6289  fresaun  6698  oev2  8448  dju0en  10089  ackbij1lem13  10144  ackbij1lem16  10147  incexclem  15792  bitsinv1  16402  bitsinvp1  16409  sadcadd  16418  sadadd2  16420  sadid1  16428  bitsres  16433  smumullem  16452  ressbas  17197  sylow2a  19585  ablfac1eu  20041  indistopon  22984  fctop  22987  cctop  22989  rest0  23152  filconn  23866  volinun  25531  itg2cnlem2  25747  pthdlem2  29854  0pth  30213  1pthdlem2  30224  disjdifprg  32664  disjun0  32684  ofpreima2  32758  of0r  32771  ldgenpisyslem1  34347  0elcarsg  34491  carsgclctunlem1  34501  carsgclctunlem3  34504  ballotlemfval0  34680  sate0  35643  elima4  36004  bj-rest10  37446  bj-rest0  37451  mblfinlem2  38025  conrel1d  44107  conrel2d  44108  ntrk0kbimka  44483  clsneibex  44546  neicvgbex  44556  qinioo  45980  nnfoctbdjlem  46898  caragen0  46949  resinsnALT  49363