Theorem eldifn 4107

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929

This theorem is referenced by:  elndif  4108  disjel  4432  tz7.7  6378  partfun  6685  funiunfv  7240  tfi  7848  peano5  7889  resf1extb  7930  frrlem11  8295  frrlem12  8296  frrlem14  8298  wfrlem10OLD  8332  wfrlem13OLD  8335  wfrlem16OLD  8338  tz7.48-2  8456  tz7.49  8459  oaf1o  8575  undifixp  8948  domdifsn  9068  isinf  9268  isinfOLD  9269  ordtypelem7  9538  unxpwdom2  9602  inf3lem3  9644  infdifsn  9671  cantnfp1lem1  9692  cantnfp1lem3  9694  cantnflem1d  9702  setind  9748  fin23lem30  10356  domtriomlem  10456  axdc3lem4  10467  axdc4lem  10469  axcclem  10471  ttukeylem7  10529  konigthlem  10582  fpwwe2lem12  10656  fpwwe2  10657  hashf1lem1  14473  rlimrecl  15596  sumrblem  15727  fsumcvg  15728  summolem2a  15731  fsumss  15741  sumss2  15742  binomlem  15845  isumltss  15864  prodrblem  15945  fprodcvg  15946  prodmolem2a  15950  fprodss  15964  fprodsplit  15982  fprodmodd  16013  sumodd  16407  prmreclem2  16937  prmreclem5  16940  ramub1lem1  17046  efgs1b  19717  gsumzsplit  19908  gsum2d  19953  gsum2d2lem  19954  dmdprdsplitlem  20020  pgpfac1lem1  20057  irredrmul  20387  lbsextlem2  21120  lbsextlem4  21122  cnsubrg  21395  psrlidm  21922  mplcoe1  21995  mplcoe5  21998  evlslem3  22038  maducoeval2  22578  madugsum  22581  elcls  23011  isclo  23025  ptbasfi  23519  ptopn2  23522  xkopt  23593  kqdisj  23670  fin1aufil  23870  ptcmplem4  23993  opnsubg  24046  tsmssplit  24090  zcld  24753  recld2  24754  reconnlem1  24766  ioombl1lem4  25514  i1fima2sn  25633  itg1val2  25637  i1f0  25640  itg1addlem4  25652  mbfi1flim  25676  itg2splitlem  25701  itg2split  25702  itg2cnlem1  25714  itg2cnlem2  25715  itgss2  25766  itgeqa  25767  itgss3  25768  itgless  25770  ibladdlem  25773  itgaddlem1  25776  iblabslem  25781  itggt0  25797  itgcn  25798  ply1termlem  26160  plypf1  26169  plyaddlem1  26170  plymullem1  26171  coeeulem  26181  coeidlem  26194  coeid3  26197  coefv0  26205  coemulc  26212  dvply1  26243  vieta1lem2  26271  aaliou2  26300  logdmnrp  26602  regamcl  27023  lgam1  27026  gam1  27027  facgam  27028  chpub  27183  chebbnd1lem1  27432  numedglnl  29123  strlem1  32231  indval2  32831  ind0  32835  cycpmco2  33144  2sqr3minply  33814  sigaclfu2  34152  eulerpartlemb  34400  mrsubcn  35541  dfon2lem6  35806  lindsadd  37637  ibladdnclem  37700  itgaddnclem1  37702  iblabsnclem  37707  ftc1anclem5  37721  ftc1anclem6  37722  ftc1anclem8  37724  dvasin  37728  dvacos  37729  pridlc2  38096  pridlc3  38097  idomnnzgmulnz  42146  deg1gprod  42153  readvrec2  42404  readvrec  42405  selvvvval  42608  fsuppssind  42616  irrapx1  42851  pellqrex  42902  qirropth  42931  setindtr  43048  kelac1  43087  flcidc  43194  arearect  43239  areaquad  43240  cantnfub  43345  mpct  45225  difmap  45231  difmapsn  45236  iccdificc  45568  fsumsupp0  45607  mccllem  45626  sumnnodd  45659  fprodcncf  45929  stoweidlem34  46063  stoweidlem44  46073  stirlinglem5  46107  fourierdlem62  46197  fouriersw  46260  elaa2lem  46262  etransclem44  46307  sge0iunmptlemfi  46442  sge0fodjrnlem  46445  meadjiunlem  46494  isomenndlem  46559  hsphoidmvle2  46614  hsphoidmvle  46615  hspdifhsp  46645  hspmbllem2  46656  ovnsubadd2lem  46674  ovolval4lem1  46678  preimagelt  46728  preimalegt  46729