Theorem in0 4353

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

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ∩ cin 3905  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-in 3913  df-nul 4288

This theorem is referenced by:  0in  4355  csbin  4408  res0  5984  dfpo2  6299  predprc  6341  fresaun  6751  oev2  8509  dju0en  10160  ackbij1lem13  10215  ackbij1lem16  10218  incexclem  15892  bitsinv1  16501  bitsinvp1  16508  sadcadd  16517  sadadd2  16519  sadid1  16527  bitsres  16532  smumullem  16551  ressbas  17297  sylow2a  19690  ablfac1eu  20146  indistopon  23139  fctop  23142  cctop  23144  rest0  23307  filconn  24021  volinun  25686  itg2cnlem2  25902  pthdlem2  30098  0pth  30457  1pthdlem2  30468  disjdifprg  32901  disjun0  32921  ofpreima2  32992  of0r  33005  ldgenpisyslem1  34534  0elcarsg  34678  carsgclctunlem1  34688  carsgclctunlem3  34691  ballotlemfval0  34867  sate0  35888  elima4  36249  bj-rest10  37711  bj-rest0  37716  mblfinlem2  38290  conrel1d  44372  conrel2d  44373  ntrk0kbimka  44748  clsneibex  44811  neicvgbex  44821  qinioo  46234  nnfoctbdjlem  47152  caragen0  47203  resinsnALT  49634