Theorem eldifn 3733

Description: Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)

Assertion

Ref	Expression
eldifn	|- ( A e. ( B \ C ) -> -. A e. C )

Proof of Theorem eldifn

Step	Hyp	Ref	Expression
1		eldif 3584	. 2 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
2	1	simprbi 480	1 |- ( A e. ( B \ C ) -> -. A e. C )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1990   \ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577

This theorem is referenced by:  elndif  3734  noel  3919  disjel  4023  tz7.7  5749  funiunfv  6506  tfi  7053  peano5  7089  wfrlem10  7424  wfrlem13  7427  wfrlem16  7430  tz7.48-2  7537  tz7.49  7540  oaf1o  7643  undifixp  7944  domdifsn  8043  isinf  8173  ordtypelem7  8429  unxpwdom2  8493  inf3lem3  8527  infdifsn  8554  cantnfp1lem1  8575  cantnfp1lem3  8577  cantnflem1d  8585  setind  8610  fin23lem30  9164  domtriomlem  9264  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  ttukeylem7  9337  konigthlem  9390  fpwwe2lem13  9464  fpwwe2  9465  hashf1lem1  13239  rlimrecl  14311  sumrblem  14442  fsumcvg  14443  summolem2a  14446  fsumss  14456  sumss2  14457  binomlem  14561  isumltss  14580  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  fprodss  14678  fprodsplit  14696  fprodmodd  14728  sumodd  15111  prmreclem2  15621  prmreclem5  15624  ramub1lem1  15730  efgs1b  18149  gsumzsplit  18327  gsum2d  18371  gsum2d2lem  18372  dmdprdsplitlem  18436  pgpfac1lem1  18473  irredrmul  18707  lbsextlem2  19159  lbsextlem4  19161  psrlidm  19403  mplcoe1  19465  mplcoe5  19468  evlslem3  19514  evlslem1  19515  cnsubrg  19806  maducoeval2  20446  madugsum  20449  elcls  20877  isclo  20891  ptbasfi  21384  ptopn2  21387  xkopt  21458  kqdisj  21535  fin1aufil  21736  ptcmplem4  21859  opnsubg  21911  tsmssplit  21955  zcld  22616  recld2  22617  reconnlem1  22629  ioombl1lem4  23329  i1fima2sn  23447  itg1val2  23451  i1f0  23454  itg1addlem4  23466  mbfi1flim  23490  itg2splitlem  23515  itg2split  23516  itg2cnlem1  23528  itg2cnlem2  23529  itgss2  23579  itgeqa  23580  itgss3  23581  itgless  23583  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  itggt0  23608  itgcn  23609  ply1termlem  23959  plypf1  23968  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeidlem  23993  coeid3  23996  coefv0  24004  coemulc  24011  dvply1  24039  vieta1lem2  24066  aaliou2  24095  logdmnrp  24387  regamcl  24787  lgam1  24790  gam1  24791  facgam  24792  chpub  24945  chebbnd1lem1  25158  numedglnl  26039  strlem1  29109  partfun  29475  elzdif0  30024  indval2  30076  ind0  30080  sigaclfu2  30184  eulerpartlemb  30430  mrsubcn  31416  dfon2lem6  31693  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem8  33492  dvasin  33496  dvacos  33497  pridlc2  33871  pridlc3  33872  irrapx1  37392  pellqrex  37443  qirropth  37473  setindtr  37591  kelac1  37633  flcidc  37744  arearect  37801  areaquad  37802  mpct  39393  difmap  39399  difmapsn  39404  iccdificc  39766  fsumsupp0  39810  mccllem  39829  sumnnodd  39862  fprodcncf  40114  stoweidlem34  40251  stoweidlem44  40261  stirlinglem5  40295  fourierdlem62  40385  fouriersw  40448  elaa2lem  40450  etransclem44  40495  sge0iunmptlemfi  40630  sge0fodjrnlem  40633  iundjiunlem  40676  meadjiunlem  40682  isomenndlem  40744  hsphoidmvle2  40799  hsphoidmvle  40800  hspdifhsp  40830  hspmbllem2  40841  ovnsubadd2lem  40859  ovolval4lem1  40863  preimagelt  40912  preimalegt  40913