Theorem eldifn 4104

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939

This theorem is referenced by:  elndif  4105  noelOLD  4297  disjel  4406  tz7.7  6217  funiunfv  7007  tfi  7568  peano5  7605  wfrlem10  7964  wfrlem13  7967  wfrlem16  7970  tz7.48-2  8078  tz7.49  8081  oaf1o  8189  undifixp  8498  domdifsn  8600  isinf  8731  ordtypelem7  8988  unxpwdom2  9052  inf3lem3  9093  infdifsn  9120  cantnfp1lem1  9141  cantnfp1lem3  9143  cantnflem1d  9151  setind  9176  fin23lem30  9764  domtriomlem  9864  axdc3lem4  9875  axdc4lem  9877  axcclem  9879  ttukeylem7  9937  konigthlem  9990  fpwwe2lem13  10064  fpwwe2  10065  hashf1lem1  13814  rlimrecl  14937  sumrblem  15068  fsumcvg  15069  summolem2a  15072  fsumss  15082  sumss2  15083  binomlem  15184  isumltss  15203  prodrblem  15283  fprodcvg  15284  prodmolem2a  15288  fprodss  15302  fprodsplit  15320  fprodmodd  15351  sumodd  15739  prmreclem2  16253  prmreclem5  16256  ramub1lem1  16362  efgs1b  18862  gsumzsplit  19047  gsum2d  19092  gsum2d2lem  19093  dmdprdsplitlem  19159  pgpfac1lem1  19196  irredrmul  19457  lbsextlem2  19931  lbsextlem4  19933  psrlidm  20183  mplcoe1  20246  mplcoe5  20249  evlslem3  20293  cnsubrg  20605  maducoeval2  21249  madugsum  21252  elcls  21681  isclo  21695  ptbasfi  22189  ptopn2  22192  xkopt  22263  kqdisj  22340  fin1aufil  22540  ptcmplem4  22663  opnsubg  22716  tsmssplit  22760  zcld  23421  recld2  23422  reconnlem1  23434  ioombl1lem4  24162  i1fima2sn  24281  itg1val2  24285  i1f0  24288  itg1addlem4  24300  mbfi1flim  24324  itg2splitlem  24349  itg2split  24350  itg2cnlem1  24362  itg2cnlem2  24363  itgss2  24413  itgeqa  24414  itgss3  24415  itgless  24417  ibladdlem  24420  itgaddlem1  24423  iblabslem  24428  itggt0  24442  itgcn  24443  ply1termlem  24793  plypf1  24802  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  coeid3  24830  coefv0  24838  coemulc  24845  dvply1  24873  vieta1lem2  24900  aaliou2  24929  logdmnrp  25224  regamcl  25638  lgam1  25641  gam1  25642  facgam  25643  chpub  25796  chebbnd1lem1  26045  numedglnl  26929  strlem1  30027  partfun  30421  cycpmco2  30775  indval2  31273  ind0  31277  sigaclfu2  31380  eulerpartlemb  31626  mrsubcn  32766  dfon2lem6  33033  frrlem11  33133  frrlem12  33134  frrlem14  33136  lindsadd  34900  ibladdnclem  34963  itgaddnclem1  34965  iblabsnclem  34970  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem8  34989  dvasin  34993  dvacos  34994  pridlc2  35365  pridlc3  35366  irrapx1  39445  pellqrex  39496  qirropth  39525  setindtr  39641  kelac1  39683  flcidc  39794  arearect  39842  areaquad  39843  mpct  41484  difmap  41490  difmapsn  41495  iccdificc  41835  fsumsupp0  41879  mccllem  41898  sumnnodd  41931  fprodcncf  42204  stoweidlem34  42339  stoweidlem44  42349  stirlinglem5  42383  fourierdlem62  42473  fouriersw  42536  elaa2lem  42538  etransclem44  42583  sge0iunmptlemfi  42715  sge0fodjrnlem  42718  iundjiunlem  42761  meadjiunlem  42767  isomenndlem  42832  hsphoidmvle2  42887  hsphoidmvle  42888  hspdifhsp  42918  hspmbllem2  42929  ovnsubadd2lem  42947  ovolval4lem1  42951  preimagelt  43000  preimalegt  43001