Theorem eldifn 4095

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

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

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 3449  df-dif 3917

This theorem is referenced by:  elndif  4096  disjel  4420  tz7.7  6358  partfun  6665  funiunfv  7222  tfi  7829  peano5  7869  resf1extb  7910  frrlem11  8275  frrlem12  8276  frrlem14  8278  tz7.48-2  8410  tz7.49  8413  oaf1o  8527  undifixp  8907  domdifsn  9024  isinf  9207  isinfOLD  9208  ordtypelem7  9477  unxpwdom2  9541  inf3lem3  9583  infdifsn  9610  cantnfp1lem1  9631  cantnfp1lem3  9633  cantnflem1d  9641  setind  9687  fin23lem30  10295  domtriomlem  10395  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  ttukeylem7  10468  konigthlem  10521  fpwwe2lem12  10595  fpwwe2  10596  hashf1lem1  14420  rlimrecl  15546  sumrblem  15677  fsumcvg  15678  summolem2a  15681  fsumss  15691  sumss2  15692  binomlem  15795  isumltss  15814  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  fprodss  15914  fprodsplit  15932  fprodmodd  15963  sumodd  16358  prmreclem2  16888  prmreclem5  16891  ramub1lem1  16997  efgs1b  19666  gsumzsplit  19857  gsum2d  19902  gsum2d2lem  19903  dmdprdsplitlem  19969  pgpfac1lem1  20006  irredrmul  20336  lbsextlem2  21069  lbsextlem4  21071  cnsubrg  21344  psrlidm  21871  mplcoe1  21944  mplcoe5  21947  evlslem3  21987  maducoeval2  22527  madugsum  22530  elcls  22960  isclo  22974  ptbasfi  23468  ptopn2  23471  xkopt  23542  kqdisj  23619  fin1aufil  23819  ptcmplem4  23942  opnsubg  23995  tsmssplit  24039  zcld  24702  recld2  24703  reconnlem1  24715  ioombl1lem4  25462  i1fima2sn  25581  itg1val2  25585  i1f0  25588  itg1addlem4  25600  mbfi1flim  25624  itg2splitlem  25649  itg2split  25650  itg2cnlem1  25662  itg2cnlem2  25663  itgss2  25714  itgeqa  25715  itgss3  25716  itgless  25718  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  itggt0  25745  itgcn  25746  ply1termlem  26108  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  coeid3  26145  coefv0  26153  coemulc  26160  dvply1  26191  vieta1lem2  26219  aaliou2  26248  logdmnrp  26550  regamcl  26971  lgam1  26974  gam1  26975  facgam  26976  chpub  27131  chebbnd1lem1  27380  numedglnl  29071  strlem1  32179  indval2  32777  ind0  32781  cycpmco2  33090  2sqr3minply  33770  sigaclfu2  34111  eulerpartlemb  34359  mrsubcn  35506  dfon2lem6  35776  lindsadd  37607  ibladdnclem  37670  itgaddnclem1  37672  iblabsnclem  37677  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem8  37694  dvasin  37698  dvacos  37699  pridlc2  38066  pridlc3  38067  idomnnzgmulnz  42121  deg1gprod  42128  readvrec2  42349  readvrec  42350  selvvvval  42573  fsuppssind  42581  irrapx1  42816  pellqrex  42867  qirropth  42896  setindtr  43013  kelac1  43052  flcidc  43159  arearect  43204  areaquad  43205  cantnfub  43310  mpct  45195  difmap  45201  difmapsn  45206  iccdificc  45537  fsumsupp0  45576  mccllem  45595  sumnnodd  45628  fprodcncf  45898  stoweidlem34  46032  stoweidlem44  46042  stirlinglem5  46076  fourierdlem62  46166  fouriersw  46229  elaa2lem  46231  etransclem44  46276  sge0iunmptlemfi  46411  sge0fodjrnlem  46414  meadjiunlem  46463  isomenndlem  46528  hsphoidmvle2  46583  hsphoidmvle  46584  hspdifhsp  46614  hspmbllem2  46625  ovnsubadd2lem  46643  ovolval4lem1  46647  preimagelt  46697  preimalegt  46698  tannpoly  46891