Theorem eldifn 4086

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 497	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906

This theorem is referenced by:  elndif  4087  disjel  4411  tz7.7  6353  partfun  6649  funiunfv  7206  tfi  7807  peano5  7847  resf1extb  7888  frrlem11  8250  frrlem12  8251  frrlem14  8253  tz7.48-2  8385  tz7.49  8388  oaf1o  8502  undifixp  8886  domdifsn  9002  isinf  9179  ordtypelem7  9443  unxpwdom2  9507  inf3lem3  9553  infdifsn  9580  cantnfp1lem1  9601  cantnfp1lem3  9603  cantnflem1d  9611  setind  9670  fin23lem30  10266  domtriomlem  10366  axdc3lem4  10377  axdc4lem  10379  axcclem  10381  ttukeylem7  10439  konigthlem  10493  fpwwe2lem12  10567  fpwwe2  10568  hashf1lem1  14392  rlimrecl  15517  sumrblem  15648  fsumcvg  15649  summolem2a  15652  fsumss  15662  sumss2  15663  binomlem  15766  isumltss  15785  prodrblem  15866  fprodcvg  15867  prodmolem2a  15871  fprodss  15885  fprodsplit  15903  fprodmodd  15934  sumodd  16329  prmreclem2  16859  prmreclem5  16862  ramub1lem1  16968  chnccat  18563  efgs1b  19682  gsumzsplit  19873  gsum2d  19918  gsum2d2lem  19919  dmdprdsplitlem  19985  pgpfac1lem1  20022  irredrmul  20380  lbsextlem2  21131  lbsextlem4  21133  cnsubrg  21399  psrlidm  21934  mplcoe1  22009  mplcoe5  22012  evlslem3  22052  maducoeval2  22601  madugsum  22604  elcls  23034  isclo  23048  ptbasfi  23542  ptopn2  23545  xkopt  23616  kqdisj  23693  fin1aufil  23893  ptcmplem4  24016  opnsubg  24069  tsmssplit  24113  zcld  24775  recld2  24776  reconnlem1  24788  ioombl1lem4  25535  i1fima2sn  25654  itg1val2  25658  i1f0  25661  itg1addlem4  25673  mbfi1flim  25697  itg2splitlem  25722  itg2split  25723  itg2cnlem1  25735  itg2cnlem2  25736  itgss2  25787  itgeqa  25788  itgss3  25789  itgless  25791  ibladdlem  25794  itgaddlem1  25797  iblabslem  25802  itggt0  25818  itgcn  25819  ply1termlem  26181  plypf1  26190  plyaddlem1  26191  plymullem1  26192  coeeulem  26202  coeidlem  26215  coeid3  26218  coefv0  26226  coemulc  26233  dvply1  26264  vieta1lem2  26292  aaliou2  26321  logdmnrp  26623  regamcl  27044  lgam1  27047  gam1  27048  facgam  27049  chpub  27204  chebbnd1lem1  27453  numedglnl  29235  strlem1  32344  indval2  32950  ind0  32954  cycpmco2  33233  2sqr3minply  33964  sigaclfu2  34305  eulerpartlemb  34552  fineqvnttrclse  35308  setindregs  35314  mrsubcn  35741  dfon2lem6  36008  lindsadd  37893  ibladdnclem  37956  itgaddnclem1  37958  iblabsnclem  37963  ftc1anclem5  37977  ftc1anclem6  37978  ftc1anclem8  37980  dvasin  37984  dvacos  37985  pridlc2  38352  pridlc3  38353  idomnnzgmulnz  42532  deg1gprod  42539  readvrec2  42760  readvrec  42761  selvvvval  42972  fsuppssind  42980  irrapx1  43214  pellqrex  43265  qirropth  43294  setindtr  43410  kelac1  43449  flcidc  43556  arearect  43601  areaquad  43602  cantnfub  43707  mpct  45588  difmap  45594  difmapsn  45599  iccdificc  45928  fsumsupp0  45967  mccllem  45986  sumnnodd  46019  fprodcncf  46287  stoweidlem34  46421  stoweidlem44  46431  stirlinglem5  46465  fourierdlem62  46555  fouriersw  46618  elaa2lem  46620  etransclem44  46665  sge0iunmptlemfi  46800  sge0fodjrnlem  46803  meadjiunlem  46852  isomenndlem  46917  hsphoidmvle2  46972  hsphoidmvle  46973  hspdifhsp  47003  hspmbllem2  47014  ovnsubadd2lem  47032  ovolval4lem1  47036  preimagelt  47086  preimalegt  47087  tannpoly  47279