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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  0in  4347  csbin  4400  res0  5974  dfpo2  6298  predprc  6340  fresaun  6751  oev2  8524  dju0en  10247  ackbij1lem13  10302  ackbij1lem16  10305  incexclem  15998  bitsinv1  16605  bitsinvp1  16612  sadcadd  16621  sadadd2  16623  sadid1  16631  bitsres  16636  smumullem  16655  ressbas  17407  sylow2a  19826  ablfac1eu  20282  indistopon  23312  fctop  23315  cctop  23317  rest0  23480  filconn  24195  volinun  25860  itg2cnlem2  26076  pthdlem2  30347  0pth  30709  1pthdlem2  30720  disjdifprg  33162  disjun0  33182  ofpreima2  33253  of0r  33266  ldgenpisyslem1  34789  0elcarsg  34932  carsgclctunlem1  34942  carsgclctunlem3  34945  ballotlemfval0  35121  sate0  36159  elima4  36520  bj-rest10  37989  bj-rest0  37994  mblfinlem2  38556  conrel1d  44648  conrel2d  44649  ntrk0kbimka  45024  clsneibex  45087  neicvgbex  45097  qinioo  46516  nnfoctbdjlem  47434  caragen0  47485  resinsnALT  49950