Theorem eldifn 4058

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886

This theorem is referenced by:  elndif  4059  disjel  4387  tz7.7  6277  partfun  6564  funiunfv  7103  tfi  7675  peano5  7714  peano5OLD  7715  frrlem11  8083  frrlem12  8084  frrlem14  8086  wfrlem10OLD  8120  wfrlem13OLD  8123  wfrlem16OLD  8126  tz7.48-2  8243  tz7.49  8246  oaf1o  8356  undifixp  8680  domdifsn  8795  isinf  8965  ordtypelem7  9213  unxpwdom2  9277  inf3lem3  9318  infdifsn  9345  cantnfp1lem1  9366  cantnfp1lem3  9368  cantnflem1d  9376  setind  9423  fin23lem30  10029  domtriomlem  10129  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  ttukeylem7  10202  konigthlem  10255  fpwwe2lem12  10329  fpwwe2  10330  hashf1lem1  14096  hashf1lem1OLD  14097  rlimrecl  15217  sumrblem  15351  fsumcvg  15352  summolem2a  15355  fsumss  15365  sumss2  15366  binomlem  15469  isumltss  15488  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  fprodss  15586  fprodsplit  15604  fprodmodd  15635  sumodd  16025  prmreclem2  16546  prmreclem5  16549  ramub1lem1  16655  efgs1b  19257  gsumzsplit  19443  gsum2d  19488  gsum2d2lem  19489  dmdprdsplitlem  19555  pgpfac1lem1  19592  irredrmul  19864  lbsextlem2  20336  lbsextlem4  20338  cnsubrg  20570  psrlidm  21082  mplcoe1  21148  mplcoe5  21151  evlslem3  21200  maducoeval2  21697  madugsum  21700  elcls  22132  isclo  22146  ptbasfi  22640  ptopn2  22643  xkopt  22714  kqdisj  22791  fin1aufil  22991  ptcmplem4  23114  opnsubg  23167  tsmssplit  23211  zcld  23882  recld2  23883  reconnlem1  23895  ioombl1lem4  24630  i1fima2sn  24749  itg1val2  24753  i1f0  24756  itg1addlem4  24768  itg1addlem4OLD  24769  mbfi1flim  24793  itg2splitlem  24818  itg2split  24819  itg2cnlem1  24831  itg2cnlem2  24832  itgss2  24882  itgeqa  24883  itgss3  24884  itgless  24886  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  itggt0  24913  itgcn  24914  ply1termlem  25269  plypf1  25278  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  coeidlem  25303  coeid3  25306  coefv0  25314  coemulc  25321  dvply1  25349  vieta1lem2  25376  aaliou2  25405  logdmnrp  25701  regamcl  26115  lgam1  26118  gam1  26119  facgam  26120  chpub  26273  chebbnd1lem1  26522  numedglnl  27417  strlem1  30513  cycpmco2  31302  indval2  31882  ind0  31886  sigaclfu2  31989  eulerpartlemb  32235  mrsubcn  33381  dfon2lem6  33670  lindsadd  35697  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem8  35784  dvasin  35788  dvacos  35789  pridlc2  36157  pridlc3  36158  fsuppssind  40205  irrapx1  40566  pellqrex  40617  qirropth  40646  setindtr  40762  kelac1  40804  flcidc  40915  arearect  40962  areaquad  40963  mpct  42630  difmap  42636  difmapsn  42641  iccdificc  42967  fsumsupp0  43009  mccllem  43028  sumnnodd  43061  fprodcncf  43331  stoweidlem34  43465  stoweidlem44  43475  stirlinglem5  43509  fourierdlem62  43599  fouriersw  43662  elaa2lem  43664  etransclem44  43709  sge0iunmptlemfi  43841  sge0fodjrnlem  43844  meadjiunlem  43893  isomenndlem  43958  hsphoidmvle2  44013  hsphoidmvle  44014  hspdifhsp  44044  hspmbllem2  44055  ovnsubadd2lem  44073  ovolval4lem1  44077  preimagelt  44126  preimalegt  44127