Theorem eldifn 4083

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906

This theorem is referenced by:  elndif  4084  disjel  4408  tz7.7  6333  partfun  6629  funiunfv  7184  tfi  7786  peano5  7826  resf1extb  7867  frrlem11  8229  frrlem12  8230  frrlem14  8232  tz7.48-2  8364  tz7.49  8367  oaf1o  8481  undifixp  8861  domdifsn  8977  isinf  9154  ordtypelem7  9416  unxpwdom2  9480  inf3lem3  9526  infdifsn  9553  cantnfp1lem1  9574  cantnfp1lem3  9576  cantnflem1d  9584  setind  9630  fin23lem30  10236  domtriomlem  10336  axdc3lem4  10347  axdc4lem  10349  axcclem  10351  ttukeylem7  10409  konigthlem  10462  fpwwe2lem12  10536  fpwwe2  10537  hashf1lem1  14362  rlimrecl  15487  sumrblem  15618  fsumcvg  15619  summolem2a  15622  fsumss  15632  sumss2  15633  binomlem  15736  isumltss  15755  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  fprodss  15855  fprodsplit  15873  fprodmodd  15904  sumodd  16299  prmreclem2  16829  prmreclem5  16832  ramub1lem1  16938  efgs1b  19615  gsumzsplit  19806  gsum2d  19851  gsum2d2lem  19852  dmdprdsplitlem  19918  pgpfac1lem1  19955  irredrmul  20312  lbsextlem2  21066  lbsextlem4  21068  cnsubrg  21334  psrlidm  21869  mplcoe1  21942  mplcoe5  21945  evlslem3  21985  maducoeval2  22525  madugsum  22528  elcls  22958  isclo  22972  ptbasfi  23466  ptopn2  23469  xkopt  23540  kqdisj  23617  fin1aufil  23817  ptcmplem4  23940  opnsubg  23993  tsmssplit  24037  zcld  24700  recld2  24701  reconnlem1  24713  ioombl1lem4  25460  i1fima2sn  25579  itg1val2  25583  i1f0  25586  itg1addlem4  25598  mbfi1flim  25622  itg2splitlem  25647  itg2split  25648  itg2cnlem1  25660  itg2cnlem2  25661  itgss2  25712  itgeqa  25713  itgss3  25714  itgless  25716  ibladdlem  25719  itgaddlem1  25722  iblabslem  25727  itggt0  25743  itgcn  25744  ply1termlem  26106  plypf1  26115  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coeidlem  26140  coeid3  26143  coefv0  26151  coemulc  26158  dvply1  26189  vieta1lem2  26217  aaliou2  26246  logdmnrp  26548  regamcl  26969  lgam1  26972  gam1  26973  facgam  26974  chpub  27129  chebbnd1lem1  27378  numedglnl  29089  strlem1  32194  indval2  32798  ind0  32802  cycpmco2  33076  2sqr3minply  33753  sigaclfu2  34094  eulerpartlemb  34342  setindregs  35071  fineqvnttrclse  35083  mrsubcn  35502  dfon2lem6  35772  lindsadd  37603  ibladdnclem  37666  itgaddnclem1  37668  iblabsnclem  37673  ftc1anclem5  37687  ftc1anclem6  37688  ftc1anclem8  37690  dvasin  37694  dvacos  37695  pridlc2  38062  pridlc3  38063  idomnnzgmulnz  42116  deg1gprod  42123  readvrec2  42344  readvrec  42345  selvvvval  42568  fsuppssind  42576  irrapx1  42811  pellqrex  42862  qirropth  42891  setindtr  43007  kelac1  43046  flcidc  43153  arearect  43198  areaquad  43199  cantnfub  43304  mpct  45189  difmap  45195  difmapsn  45200  iccdificc  45530  fsumsupp0  45569  mccllem  45588  sumnnodd  45621  fprodcncf  45891  stoweidlem34  46025  stoweidlem44  46035  stirlinglem5  46069  fourierdlem62  46159  fouriersw  46222  elaa2lem  46224  etransclem44  46269  sge0iunmptlemfi  46404  sge0fodjrnlem  46407  meadjiunlem  46456  isomenndlem  46521  hsphoidmvle2  46576  hsphoidmvle  46577  hspdifhsp  46607  hspmbllem2  46618  ovnsubadd2lem  46636  ovolval4lem1  46640  preimagelt  46690  preimalegt  46691  tannpoly  46884