Theorem eldifn 4063

Description: Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)

Assertion

Ref	Expression
eldifn	⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)

Proof of Theorem eldifn

Step	Hyp	Ref	Expression
1		eldif 3898	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
2	1	simprbi 497	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891

This theorem is referenced by:  elndif  4064  disjel  4391  tz7.7  6296  partfun  6589  funiunfv  7130  tfi  7709  peano5  7749  peano5OLD  7750  frrlem11  8121  frrlem12  8122  frrlem14  8124  wfrlem10OLD  8158  wfrlem13OLD  8161  wfrlem16OLD  8164  tz7.48-2  8282  tz7.49  8285  oaf1o  8403  undifixp  8731  domdifsn  8850  isinf  9045  ordtypelem7  9292  unxpwdom2  9356  inf3lem3  9397  infdifsn  9424  cantnfp1lem1  9445  cantnfp1lem3  9447  cantnflem1d  9455  setind  9501  fin23lem30  10107  domtriomlem  10207  axdc3lem4  10218  axdc4lem  10220  axcclem  10222  ttukeylem7  10280  konigthlem  10333  fpwwe2lem12  10407  fpwwe2  10408  hashf1lem1  14177  hashf1lem1OLD  14178  rlimrecl  15298  sumrblem  15432  fsumcvg  15433  summolem2a  15436  fsumss  15446  sumss2  15447  binomlem  15550  isumltss  15569  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  fprodss  15667  fprodsplit  15685  fprodmodd  15716  sumodd  16106  prmreclem2  16627  prmreclem5  16630  ramub1lem1  16736  efgs1b  19351  gsumzsplit  19537  gsum2d  19582  gsum2d2lem  19583  dmdprdsplitlem  19649  pgpfac1lem1  19686  irredrmul  19958  lbsextlem2  20430  lbsextlem4  20432  cnsubrg  20667  psrlidm  21181  mplcoe1  21247  mplcoe5  21250  evlslem3  21299  maducoeval2  21798  madugsum  21801  elcls  22233  isclo  22247  ptbasfi  22741  ptopn2  22744  xkopt  22815  kqdisj  22892  fin1aufil  23092  ptcmplem4  23215  opnsubg  23268  tsmssplit  23312  zcld  23985  recld2  23986  reconnlem1  23998  ioombl1lem4  24734  i1fima2sn  24853  itg1val2  24857  i1f0  24860  itg1addlem4  24872  itg1addlem4OLD  24873  mbfi1flim  24897  itg2splitlem  24922  itg2split  24923  itg2cnlem1  24935  itg2cnlem2  24936  itgss2  24986  itgeqa  24987  itgss3  24988  itgless  24990  ibladdlem  24993  itgaddlem1  24996  iblabslem  25001  itggt0  25017  itgcn  25018  ply1termlem  25373  plypf1  25382  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  coeidlem  25407  coeid3  25410  coefv0  25418  coemulc  25425  dvply1  25453  vieta1lem2  25480  aaliou2  25509  logdmnrp  25805  regamcl  26219  lgam1  26222  gam1  26223  facgam  26224  chpub  26377  chebbnd1lem1  26626  numedglnl  27523  strlem1  30621  cycpmco2  31409  indval2  31991  ind0  31995  sigaclfu2  32098  eulerpartlemb  32344  mrsubcn  33490  dfon2lem6  33773  lindsadd  35779  ibladdnclem  35842  itgaddnclem1  35844  iblabsnclem  35849  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem8  35866  dvasin  35870  dvacos  35871  pridlc2  36239  pridlc3  36240  fsuppssind  40289  prjcrv0  40477  irrapx1  40657  pellqrex  40708  qirropth  40737  setindtr  40853  kelac1  40895  flcidc  41006  arearect  41053  areaquad  41054  mpct  42748  difmap  42754  difmapsn  42759  iccdificc  43084  fsumsupp0  43126  mccllem  43145  sumnnodd  43178  fprodcncf  43448  stoweidlem34  43582  stoweidlem44  43592  stirlinglem5  43626  fourierdlem62  43716  fouriersw  43779  elaa2lem  43781  etransclem44  43826  sge0iunmptlemfi  43958  sge0fodjrnlem  43961  meadjiunlem  44010  isomenndlem  44075  hsphoidmvle2  44130  hsphoidmvle  44131  hspdifhsp  44161  hspmbllem2  44172  ovnsubadd2lem  44190  ovolval4lem1  44194  preimagelt  44244  preimalegt  44245