Theorem eldifn 4082

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902

This theorem is referenced by:  elndif  4083  disjel  4407  tz7.7  6341  partfun  6637  funiunfv  7192  tfi  7793  peano5  7833  resf1extb  7874  frrlem11  8236  frrlem12  8237  frrlem14  8239  tz7.48-2  8371  tz7.49  8374  oaf1o  8488  undifixp  8870  domdifsn  8986  isinf  9163  ordtypelem7  9427  unxpwdom2  9491  inf3lem3  9537  infdifsn  9564  cantnfp1lem1  9585  cantnfp1lem3  9587  cantnflem1d  9595  setind  9654  fin23lem30  10250  domtriomlem  10350  axdc3lem4  10361  axdc4lem  10363  axcclem  10365  ttukeylem7  10423  konigthlem  10477  fpwwe2lem12  10551  fpwwe2  10552  hashf1lem1  14376  rlimrecl  15501  sumrblem  15632  fsumcvg  15633  summolem2a  15636  fsumss  15646  sumss2  15647  binomlem  15750  isumltss  15769  prodrblem  15850  fprodcvg  15851  prodmolem2a  15855  fprodss  15869  fprodsplit  15887  fprodmodd  15918  sumodd  16313  prmreclem2  16843  prmreclem5  16846  ramub1lem1  16952  chnccat  18547  efgs1b  19663  gsumzsplit  19854  gsum2d  19899  gsum2d2lem  19900  dmdprdsplitlem  19966  pgpfac1lem1  20003  irredrmul  20361  lbsextlem2  21112  lbsextlem4  21114  cnsubrg  21380  psrlidm  21915  mplcoe1  21990  mplcoe5  21993  evlslem3  22033  maducoeval2  22582  madugsum  22585  elcls  23015  isclo  23029  ptbasfi  23523  ptopn2  23526  xkopt  23597  kqdisj  23674  fin1aufil  23874  ptcmplem4  23997  opnsubg  24050  tsmssplit  24094  zcld  24756  recld2  24757  reconnlem1  24769  ioombl1lem4  25516  i1fima2sn  25635  itg1val2  25639  i1f0  25642  itg1addlem4  25654  mbfi1flim  25678  itg2splitlem  25703  itg2split  25704  itg2cnlem1  25716  itg2cnlem2  25717  itgss2  25768  itgeqa  25769  itgss3  25770  itgless  25772  ibladdlem  25775  itgaddlem1  25778  iblabslem  25783  itggt0  25799  itgcn  25800  ply1termlem  26162  plypf1  26171  plyaddlem1  26172  plymullem1  26173  coeeulem  26183  coeidlem  26196  coeid3  26199  coefv0  26207  coemulc  26214  dvply1  26245  vieta1lem2  26273  aaliou2  26302  logdmnrp  26604  regamcl  27025  lgam1  27028  gam1  27029  facgam  27030  chpub  27185  chebbnd1lem1  27434  numedglnl  29166  strlem1  32274  indval2  32882  ind0  32886  cycpmco2  33164  2sqr3minply  33886  sigaclfu2  34227  eulerpartlemb  34474  fineqvnttrclse  35229  setindregs  35235  mrsubcn  35662  dfon2lem6  35929  lindsadd  37753  ibladdnclem  37816  itgaddnclem1  37818  iblabsnclem  37823  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem8  37840  dvasin  37844  dvacos  37845  pridlc2  38212  pridlc3  38213  idomnnzgmulnz  42326  deg1gprod  42333  readvrec2  42558  readvrec  42559  selvvvval  42770  fsuppssind  42778  irrapx1  43012  pellqrex  43063  qirropth  43092  setindtr  43208  kelac1  43247  flcidc  43354  arearect  43399  areaquad  43400  cantnfub  43505  mpct  45387  difmap  45393  difmapsn  45398  iccdificc  45727  fsumsupp0  45766  mccllem  45785  sumnnodd  45818  fprodcncf  46086  stoweidlem34  46220  stoweidlem44  46230  stirlinglem5  46264  fourierdlem62  46354  fouriersw  46417  elaa2lem  46419  etransclem44  46464  sge0iunmptlemfi  46599  sge0fodjrnlem  46602  meadjiunlem  46651  isomenndlem  46716  hsphoidmvle2  46771  hsphoidmvle  46772  hspdifhsp  46802  hspmbllem2  46813  ovnsubadd2lem  46831  ovolval4lem1  46835  preimagelt  46885  preimalegt  46886  tannpoly  47078