Theorem in0 3968

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 3919	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 966	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 214	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 3806	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ∩ cin 3573  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-nul 3916

This theorem is referenced by:  0in  3969  csbin  4010  res0  5400  fresaun  6075  oev2  7603  cda0en  9001  ackbij1lem13  9054  ackbij1lem16  9057  incexclem  14568  bitsinv1  15164  bitsinvp1  15171  sadcadd  15180  sadadd2  15182  sadid1  15190  bitsres  15195  smumullem  15214  ressbas  15930  sylow2a  18034  ablfac1eu  18472  indistopon  20805  fctop  20808  cctop  20810  rest0  20973  filconn  21687  volinun  23314  itg2cnlem2  23529  pthdlem2  26664  0pth  26986  1pthdlem2  26996  disjdifprg  29388  disjun0  29408  ofpreima2  29466  ldgenpisyslem1  30226  0elcarsg  30369  carsgclctunlem1  30379  carsgclctunlem3  30382  ballotlemfval0  30557  dfpo2  31645  elima4  31679  bj-rest10  33041  bj-rest0  33046  mblfinlem2  33447  conrel1d  37955  conrel2d  37956  ntrk0kbimka  38337  clsneibex  38400  neicvgbex  38410  qinioo  39762  nnfoctbdjlem  40672  caragen0  40720