Theorem eldifn 4016

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 3851	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
2	1	simprbi 500	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ∖ cdif 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-dif 3844

This theorem is referenced by:  elndif  4017  disjel  4343  tz7.7  6192  partfun  6478  funiunfv  7012  tfi  7581  peano5  7618  wfrlem10  7986  wfrlem13  7989  wfrlem16  7992  tz7.48-2  8100  tz7.49  8103  oaf1o  8213  undifixp  8537  domdifsn  8642  isinf  8803  ordtypelem7  9054  unxpwdom2  9118  inf3lem3  9159  infdifsn  9186  cantnfp1lem1  9207  cantnfp1lem3  9209  cantnflem1d  9217  setind  9242  fin23lem30  9835  domtriomlem  9935  axdc3lem4  9946  axdc4lem  9948  axcclem  9950  ttukeylem7  10008  konigthlem  10061  fpwwe2lem12  10135  fpwwe2  10136  hashf1lem1  13899  hashf1lem1OLD  13900  rlimrecl  15020  sumrblem  15154  fsumcvg  15155  summolem2a  15158  fsumss  15168  sumss2  15169  binomlem  15270  isumltss  15289  prodrblem  15368  fprodcvg  15369  prodmolem2a  15373  fprodss  15387  fprodsplit  15405  fprodmodd  15436  sumodd  15826  prmreclem2  16346  prmreclem5  16349  ramub1lem1  16455  efgs1b  18973  gsumzsplit  19159  gsum2d  19204  gsum2d2lem  19205  dmdprdsplitlem  19271  pgpfac1lem1  19308  irredrmul  19572  lbsextlem2  20043  lbsextlem4  20045  cnsubrg  20270  psrlidm  20775  mplcoe1  20841  mplcoe5  20844  evlslem3  20887  maducoeval2  21384  madugsum  21387  elcls  21817  isclo  21831  ptbasfi  22325  ptopn2  22328  xkopt  22399  kqdisj  22476  fin1aufil  22676  ptcmplem4  22799  opnsubg  22852  tsmssplit  22896  zcld  23558  recld2  23559  reconnlem1  23571  ioombl1lem4  24306  i1fima2sn  24425  itg1val2  24429  i1f0  24432  itg1addlem4  24444  mbfi1flim  24468  itg2splitlem  24493  itg2split  24494  itg2cnlem1  24506  itg2cnlem2  24507  itgss2  24557  itgeqa  24558  itgss3  24559  itgless  24561  ibladdlem  24564  itgaddlem1  24567  iblabslem  24572  itggt0  24588  itgcn  24589  ply1termlem  24944  plypf1  24953  plyaddlem1  24954  plymullem1  24955  coeeulem  24965  coeidlem  24978  coeid3  24981  coefv0  24989  coemulc  24996  dvply1  25024  vieta1lem2  25051  aaliou2  25080  logdmnrp  25376  regamcl  25790  lgam1  25793  gam1  25794  facgam  25795  chpub  25948  chebbnd1lem1  26197  numedglnl  27081  strlem1  30177  cycpmco2  30969  indval2  31544  ind0  31548  sigaclfu2  31651  eulerpartlemb  31897  mrsubcn  33044  dfon2lem6  33328  frrlem11  33443  frrlem12  33444  frrlem14  33446  lindsadd  35382  ibladdnclem  35445  itgaddnclem1  35447  iblabsnclem  35452  ftc1anclem5  35466  ftc1anclem6  35467  ftc1anclem8  35469  dvasin  35473  dvacos  35474  pridlc2  35842  pridlc3  35843  fsuppssind  39845  irrapx1  40206  pellqrex  40257  qirropth  40286  setindtr  40402  kelac1  40444  flcidc  40555  arearect  40602  areaquad  40603  mpct  42263  difmap  42269  difmapsn  42274  iccdificc  42601  fsumsupp0  42645  mccllem  42664  sumnnodd  42697  fprodcncf  42967  stoweidlem34  43101  stoweidlem44  43111  stirlinglem5  43145  fourierdlem62  43235  fouriersw  43298  elaa2lem  43300  etransclem44  43345  sge0iunmptlemfi  43477  sge0fodjrnlem  43480  meadjiunlem  43529  isomenndlem  43594  hsphoidmvle2  43649  hsphoidmvle  43650  hspdifhsp  43680  hspmbllem2  43691  ovnsubadd2lem  43709  ovolval4lem1  43713  preimagelt  43762  preimalegt  43763