Theorem in0 4336

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 4279	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 533	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4153	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∩ cin 3889  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275

This theorem is referenced by:  0in  4338  csbin  4383  res0  5942  dfpo2  6254  predprc  6296  fresaun  6705  oev2  8451  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  22976  fctop  22979  cctop  22981  rest0  23144  filconn  23858  volinun  25523  itg2cnlem2  25739  pthdlem2  29851  0pth  30210  1pthdlem2  30221  disjdifprg  32660  disjun0  32680  ofpreima2  32754  of0r  32767  ldgenpisyslem1  34323  0elcarsg  34467  carsgclctunlem1  34477  carsgclctunlem3  34480  ballotlemfval0  34656  sate0  35613  elima4  35974  bj-rest10  37416  bj-rest0  37421  mblfinlem2  37993  conrel1d  44108  conrel2d  44109  ntrk0kbimka  44484  clsneibex  44547  neicvgbex  44557  qinioo  45983  nnfoctbdjlem  46901  caragen0  46952  resinsnALT  49360