Theorem eldifn 4071

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147   ∖ cdif 4048

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050

This theorem is used by:  elndif  4072  disjel  4413  tz7.7  6403  partfun  6705  funiunfv  7272  tfi  7885  peano5  7926  resf1extb  7967  frrlem11  8339  frrlem12  8340  frrlem14  8342  tz7.48-2  8477  tz7.49  8480  oaf1o  8596  undifixp  8987  domdifsn  9104  isinf  9281  ordtypelem7  9542  unxpwdom2  9606  inf3lem3  9655  infdifsn  9682  cantnfp1lem1  9703  cantnfp1lem3  9705  cantnflem1d  9713  setind  9772  fin23lem30  10444  domtriomlem  10544  axdc3lem4  10555  axdc4lem  10557  axcclem  10559  ttukeylem7  10617  konigthlem  10677  fpwwe2lem12  10751  fpwwe2  10752  indval2  12349  ind0  12354  hashf1lem1  14624  rlimrecl  15773  sumrblem  15903  fsumcvg  15904  summolem2a  15907  fsumss  15917  sumss2  15918  binomlem  16024  isumltss  16043  prodrblem  16122  fprodcvg  16123  prodmolem2a  16127  fprodss  16141  fprodsplit  16159  fprodmodd  16190  sumodd  16584  prmreclem2  17121  prmreclem5  17124  ramub1lem1  17230  chnccat  18826  efgs1b  19977  gsumzsplit  20168  gsum2d  20213  gsum2d2lem  20214  dmdprdsplitlem  20280  pgpfac1lem1  20317  irredrmul  20684  lbsextlem2  21464  lbsextlem4  21466  prmidlc2  21657  cmprmidlmcl  21658  cnsubrg  21760  psrlidm  22296  mplcoe1  22373  mplcoe5  22376  evlslem3  22416  selvvvval  22478  maducoeval2  22982  madugsum  22985  elcls  23418  isclo  23432  ptbasfi  23927  ptopn2  23930  xkopt  24001  kqdisj  24078  fin1aufil  24278  ptcmplem4  24401  opnsubg  24454  tsmssplit  24498  zcld  25160  recld2  25161  reconnlem1  25173  ioombl1lem4  25909  i1fima2sn  26028  itg1val2  26032  i1f0  26035  itg1addlem4  26047  mbfi1flim  26071  itg2splitlem  26096  itg2split  26097  itg2cnlem1  26109  itg2cnlem2  26110  itgss2  26160  itgeqa  26161  itgss3  26162  itgless  26164  ibladdlem  26167  itgaddlem1  26170  iblabslem  26175  itggt0  26191  itgcn  26192  ply1termlem  26548  plypf1  26558  plyaddlem1  26559  plymullem1  26560  coeeulem  26570  coeidlem  26583  coeid3  26586  coefv0  26594  coemulc  26601  dvply1  26632  vieta1lem2  26661  aaliou2  26694  logdmnrp  26996  regamcl  27415  lgam1  27418  gam1  27419  facgam  27420  chpub  27574  chebbnd1lem1  27823  numedglnl  29749  strlem1  32879  cycpmco2  33761  2sqr3minply  34479  sigaclfu2  34820  eulerpartlemb  35067  acwer1prc  35851  fineqvnttrclse  35891  setindregs  35897  mrsubcn  36450  dfon2lem6  36727  lindsadd  38727  ibladdnclem  38785  itgaddnclem1  38787  iblabsnclem  38792  ftc1anclem5  38806  ftc1anclem6  38807  ftc1anclem8  38809  dvasin  38813  dvacos  38814  pridlc2  39197  pridlc3  39198  idomnnzgmulnz  43374  deg1gprod  43381  readvrec2  43603  readvrec  43604  fsuppssind  43812  irrapx1  44026  pellqrex  44077  qirropth  44106  setindtr  44222  kelac1  44256  flcidc  44362  arearect  44407  areaquad  44408  cantnfub  44513  mpct  46418  difmap  46423  difmapsn  46428  iccdificc  46754  fsumsupp0  46793  mccllem  46812  sumnnodd  46845  fprodcncf  47113  stoweidlem34  47247  stoweidlem44  47257  stirlinglem5  47291  fourierdlem62  47381  fouriersw  47444  elaa2lem  47446  etransclem44  47491  sge0iunmptlemfi  47626  sge0fodjrnlem  47629  meadjiunlem  47678  isomenndlem  47743  hsphoidmvle2  47798  hsphoidmvle  47799  hspdifhsp  47829  hspmbllem2  47840  ovnsubadd2lem  47858  ovolval4lem1  47862  preimagelt  47912  preimalegt  47913  tannpoly  48143  tmachlem-tpopen  48154