Theorem eldifn 4065

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2121   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3888

This theorem is referenced by:  elndif  4066  disjel  4388  tz7.7  6340  partfun  6636  funiunfv  7196  tfi  7797  peano5  7837  resf1extb  7878  frrlem11  8240  frrlem12  8241  frrlem14  8243  tz7.48-2  8375  tz7.49  8378  oaf1o  8492  undifixp  8876  domdifsn  8992  isinf  9169  ordtypelem7  9433  unxpwdom2  9497  inf3lem3  9546  infdifsn  9573  cantnfp1lem1  9594  cantnfp1lem3  9596  cantnflem1d  9604  setind  9663  fin23lem30  10259  domtriomlem  10359  axdc3lem4  10370  axdc4lem  10372  axcclem  10374  ttukeylem7  10432  konigthlem  10486  fpwwe2lem12  10560  fpwwe2  10561  indval2  12159  ind0  12164  hashf1lem1  14412  rlimrecl  15537  sumrblem  15668  fsumcvg  15669  summolem2a  15672  fsumss  15682  sumss2  15683  binomlem  15789  isumltss  15808  prodrblem  15889  fprodcvg  15890  prodmolem2a  15894  fprodss  15908  fprodsplit  15926  fprodmodd  15957  sumodd  16352  prmreclem2  16883  prmreclem5  16886  ramub1lem1  16992  chnccat  18587  efgs1b  19706  gsumzsplit  19897  gsum2d  19942  gsum2d2lem  19943  dmdprdsplitlem  20009  pgpfac1lem1  20046  irredrmul  20402  lbsextlem2  21156  lbsextlem4  21158  cnsubrg  21406  psrlidm  21940  mplcoe1  22017  mplcoe5  22020  evlslem3  22060  selvvvval  22122  maducoeval2  22627  madugsum  22630  elcls  23060  isclo  23074  ptbasfi  23568  ptopn2  23571  xkopt  23642  kqdisj  23719  fin1aufil  23919  ptcmplem4  24042  opnsubg  24095  tsmssplit  24139  zcld  24801  recld2  24802  reconnlem1  24814  ioombl1lem4  25550  i1fima2sn  25669  itg1val2  25673  i1f0  25676  itg1addlem4  25688  mbfi1flim  25712  itg2splitlem  25737  itg2split  25738  itg2cnlem1  25750  itg2cnlem2  25751  itgss2  25802  itgeqa  25803  itgss3  25804  itgless  25806  ibladdlem  25809  itgaddlem1  25812  iblabslem  25817  itggt0  25833  itgcn  25834  ply1termlem  26190  plypf1  26199  plyaddlem1  26200  plymullem1  26201  coeeulem  26211  coeidlem  26224  coeid3  26227  coefv0  26235  coemulc  26242  dvply1  26272  vieta1lem2  26299  aaliou2  26328  logdmnrp  26627  regamcl  27046  lgam1  27049  gam1  27050  facgam  27051  chpub  27205  chebbnd1lem1  27454  numedglnl  29235  strlem1  32343  cycpmco2  33218  2sqr3minply  33976  sigaclfu2  34317  eulerpartlemb  34564  fineqvnttrclse  35320  setindregs  35326  mrsubcn  35762  dfon2lem6  36029  lindsadd  37995  ibladdnclem  38058  itgaddnclem1  38060  iblabsnclem  38065  ftc1anclem5  38079  ftc1anclem6  38080  ftc1anclem8  38082  dvasin  38086  dvacos  38087  pridlc2  38454  pridlc3  38455  idomnnzgmulnz  42633  deg1gprod  42640  readvrec2  42853  readvrec  42854  fsuppssind  43058  irrapx1  43288  pellqrex  43339  qirropth  43368  setindtr  43484  kelac1  43523  flcidc  43630  arearect  43675  areaquad  43676  cantnfub  43781  mpct  45661  difmap  45666  difmapsn  45671  iccdificc  45998  fsumsupp0  46037  mccllem  46056  sumnnodd  46089  fprodcncf  46357  stoweidlem34  46491  stoweidlem44  46501  stirlinglem5  46535  fourierdlem62  46625  fouriersw  46688  elaa2lem  46690  etransclem44  46735  sge0iunmptlemfi  46870  sge0fodjrnlem  46873  meadjiunlem  46922  isomenndlem  46987  hsphoidmvle2  47042  hsphoidmvle  47043  hspdifhsp  47073  hspmbllem2  47084  ovnsubadd2lem  47102  ovolval4lem1  47106  preimagelt  47156  preimalegt  47157  tannpoly  47367