Theorem eldifn 4098

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920

This theorem is referenced by:  elndif  4099  disjel  4423  tz7.7  6361  partfun  6668  funiunfv  7225  tfi  7832  peano5  7872  resf1extb  7913  frrlem11  8278  frrlem12  8279  frrlem14  8281  tz7.48-2  8413  tz7.49  8416  oaf1o  8530  undifixp  8910  domdifsn  9028  isinf  9214  isinfOLD  9215  ordtypelem7  9484  unxpwdom2  9548  inf3lem3  9590  infdifsn  9617  cantnfp1lem1  9638  cantnfp1lem3  9640  cantnflem1d  9648  setind  9694  fin23lem30  10302  domtriomlem  10402  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  ttukeylem7  10475  konigthlem  10528  fpwwe2lem12  10602  fpwwe2  10603  hashf1lem1  14427  rlimrecl  15553  sumrblem  15684  fsumcvg  15685  summolem2a  15688  fsumss  15698  sumss2  15699  binomlem  15802  isumltss  15821  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  fprodss  15921  fprodsplit  15939  fprodmodd  15970  sumodd  16365  prmreclem2  16895  prmreclem5  16898  ramub1lem1  17004  efgs1b  19673  gsumzsplit  19864  gsum2d  19909  gsum2d2lem  19910  dmdprdsplitlem  19976  pgpfac1lem1  20013  irredrmul  20343  lbsextlem2  21076  lbsextlem4  21078  cnsubrg  21351  psrlidm  21878  mplcoe1  21951  mplcoe5  21954  evlslem3  21994  maducoeval2  22534  madugsum  22537  elcls  22967  isclo  22981  ptbasfi  23475  ptopn2  23478  xkopt  23549  kqdisj  23626  fin1aufil  23826  ptcmplem4  23949  opnsubg  24002  tsmssplit  24046  zcld  24709  recld2  24710  reconnlem1  24722  ioombl1lem4  25469  i1fima2sn  25588  itg1val2  25592  i1f0  25595  itg1addlem4  25607  mbfi1flim  25631  itg2splitlem  25656  itg2split  25657  itg2cnlem1  25669  itg2cnlem2  25670  itgss2  25721  itgeqa  25722  itgss3  25723  itgless  25725  ibladdlem  25728  itgaddlem1  25731  iblabslem  25736  itggt0  25752  itgcn  25753  ply1termlem  26115  plypf1  26124  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeidlem  26149  coeid3  26152  coefv0  26160  coemulc  26167  dvply1  26198  vieta1lem2  26226  aaliou2  26255  logdmnrp  26557  regamcl  26978  lgam1  26981  gam1  26982  facgam  26983  chpub  27138  chebbnd1lem1  27387  numedglnl  29078  strlem1  32186  indval2  32784  ind0  32788  cycpmco2  33097  2sqr3minply  33777  sigaclfu2  34118  eulerpartlemb  34366  mrsubcn  35513  dfon2lem6  35783  lindsadd  37614  ibladdnclem  37677  itgaddnclem1  37679  iblabsnclem  37684  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem8  37701  dvasin  37705  dvacos  37706  pridlc2  38073  pridlc3  38074  idomnnzgmulnz  42128  deg1gprod  42135  readvrec2  42356  readvrec  42357  selvvvval  42580  fsuppssind  42588  irrapx1  42823  pellqrex  42874  qirropth  42903  setindtr  43020  kelac1  43059  flcidc  43166  arearect  43211  areaquad  43212  cantnfub  43317  mpct  45202  difmap  45208  difmapsn  45213  iccdificc  45544  fsumsupp0  45583  mccllem  45602  sumnnodd  45635  fprodcncf  45905  stoweidlem34  46039  stoweidlem44  46049  stirlinglem5  46083  fourierdlem62  46173  fouriersw  46236  elaa2lem  46238  etransclem44  46283  sge0iunmptlemfi  46418  sge0fodjrnlem  46421  meadjiunlem  46470  isomenndlem  46535  hsphoidmvle2  46590  hsphoidmvle  46591  hspdifhsp  46621  hspmbllem2  46632  ovnsubadd2lem  46650  ovolval4lem1  46654  preimagelt  46704  preimalegt  46705