Theorem eldifn 4082

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ∖ cdif 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905

This theorem is used by:  elndif  4083  disjel  4413  tz7.7  6387  partfun  6683  funiunfv  7248  tfi  7852  peano5  7893  resf1extb  7934  frrlem11  8298  frrlem12  8299  frrlem14  8301  tz7.48-2  8434  tz7.49  8437  oaf1o  8553  undifixp  8944  domdifsn  9061  isinf  9238  ordtypelem7  9499  unxpwdom2  9563  inf3lem3  9612  infdifsn  9639  cantnfp1lem1  9660  cantnfp1lem3  9662  cantnflem1d  9670  setind  9729  fin23lem30  10347  domtriomlem  10447  axdc3lem4  10458  axdc4lem  10460  axcclem  10462  ttukeylem7  10520  konigthlem  10578  fpwwe2lem12  10652  fpwwe2  10653  indval2  12248  ind0  12253  hashf1lem1  14520  rlimrecl  15667  sumrblem  15797  fsumcvg  15798  summolem2a  15801  fsumss  15811  sumss2  15812  binomlem  15918  isumltss  15937  prodrblem  16018  fprodcvg  16019  prodmolem2a  16023  fprodss  16037  fprodsplit  16055  fprodmodd  16086  sumodd  16480  prmreclem2  17011  prmreclem5  17014  ramub1lem1  17120  chnccat  18716  efgs1b  19862  gsumzsplit  20053  gsum2d  20098  gsum2d2lem  20099  dmdprdsplitlem  20165  pgpfac1lem1  20202  irredrmul  20567  lbsextlem2  21345  lbsextlem4  21347  prmidlc2  21536  cmprmidlmcl  21537  cnsubrg  21639  psrlidm  22175  mplcoe1  22252  mplcoe5  22255  evlslem3  22295  selvvvval  22357  maducoeval2  22861  madugsum  22864  elcls  23297  isclo  23311  ptbasfi  23806  ptopn2  23809  xkopt  23880  kqdisj  23957  fin1aufil  24157  ptcmplem4  24280  opnsubg  24333  tsmssplit  24377  zcld  25039  recld2  25040  reconnlem1  25052  ioombl1lem4  25788  i1fima2sn  25907  itg1val2  25911  i1f0  25914  itg1addlem4  25926  mbfi1flim  25950  itg2splitlem  25975  itg2split  25976  itg2cnlem1  25988  itg2cnlem2  25989  itgss2  26040  itgeqa  26041  itgss3  26042  itgless  26044  ibladdlem  26047  itgaddlem1  26050  iblabslem  26055  itggt0  26071  itgcn  26072  ply1termlem  26428  plypf1  26437  plyaddlem1  26438  plymullem1  26439  coeeulem  26449  coeidlem  26462  coeid3  26465  coefv0  26473  coemulc  26480  dvply1  26513  vieta1lem2  26540  aaliou2  26571  logdmnrp  26874  regamcl  27293  lgam1  27296  gam1  27297  facgam  27298  chpub  27452  chebbnd1lem1  27701  numedglnl  29585  strlem1  32715  cycpmco2  33558  2sqr3minply  34275  sigaclfu2  34616  eulerpartlemb  34864  fineqvnttrclse  35635  setindregs  35641  mrsubcn  36083  dfon2lem6  36350  lindsadd  38352  ibladdnclem  38410  itgaddnclem1  38412  iblabsnclem  38417  ftc1anclem5  38431  ftc1anclem6  38432  ftc1anclem8  38434  dvasin  38438  dvacos  38439  pridlc2  38807  pridlc3  38808  idomnnzgmulnz  42984  deg1gprod  42991  readvrec2  43221  readvrec  43222  fsuppssind  43424  irrapx1  43654  pellqrex  43705  qirropth  43734  setindtr  43850  kelac1  43889  flcidc  43996  arearect  44041  areaquad  44042  cantnfub  44147  mpct  46017  difmap  46022  difmapsn  46027  iccdificc  46354  fsumsupp0  46393  mccllem  46412  sumnnodd  46445  fprodcncf  46713  stoweidlem34  46847  stoweidlem44  46857  stirlinglem5  46891  fourierdlem62  46981  fouriersw  47044  elaa2lem  47046  etransclem44  47091  sge0iunmptlemfi  47226  sge0fodjrnlem  47229  meadjiunlem  47278  isomenndlem  47343  hsphoidmvle2  47398  hsphoidmvle  47399  hspdifhsp  47429  hspmbllem2  47440  ovnsubadd2lem  47458  ovolval4lem1  47462  preimagelt  47512  preimalegt  47513  tannpoly  47743  tmachlem-tpopen  47754