Theorem eldifn 4086

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908

This theorem is used by:  elndif  4087  disjel  4417  tz7.7  6386  partfun  6682  funiunfv  7246  tfi  7845  peano5  7886  resf1extb  7927  frrlem11  8289  frrlem12  8290  frrlem14  8292  tz7.48-2  8425  tz7.49  8428  oaf1o  8544  undifixp  8928  domdifsn  9044  isinf  9221  ordtypelem7  9482  unxpwdom2  9546  inf3lem3  9595  infdifsn  9622  cantnfp1lem1  9643  cantnfp1lem3  9645  cantnflem1d  9653  setind  9712  fin23lem30  10330  domtriomlem  10430  axdc3lem4  10441  axdc4lem  10443  axcclem  10445  ttukeylem7  10503  konigthlem  10557  fpwwe2lem12  10631  fpwwe2  10632  indval2  12227  ind0  12232  hashf1lem1  14497  rlimrecl  15636  sumrblem  15767  fsumcvg  15768  summolem2a  15771  fsumss  15781  sumss2  15782  binomlem  15888  isumltss  15907  prodrblem  15988  fprodcvg  15989  prodmolem2a  15993  fprodss  16007  fprodsplit  16025  fprodmodd  16056  sumodd  16450  prmreclem2  16981  prmreclem5  16984  ramub1lem1  17090  chnccat  18686  efgs1b  19810  gsumzsplit  20001  gsum2d  20046  gsum2d2lem  20047  dmdprdsplitlem  20113  pgpfac1lem1  20150  irredrmul  20514  lbsextlem2  21292  lbsextlem4  21294  prmidlc2  21483  cmprmidlmcl  21484  cnsubrg  21586  psrlidm  22120  mplcoe1  22197  mplcoe5  22200  evlslem3  22240  selvvvval  22302  maducoeval2  22806  madugsum  22809  elcls  23239  isclo  23253  ptbasfi  23747  ptopn2  23750  xkopt  23821  kqdisj  23898  fin1aufil  24098  ptcmplem4  24221  opnsubg  24274  tsmssplit  24318  zcld  24980  recld2  24981  reconnlem1  24993  ioombl1lem4  25729  i1fima2sn  25848  itg1val2  25852  i1f0  25855  itg1addlem4  25867  mbfi1flim  25891  itg2splitlem  25916  itg2split  25917  itg2cnlem1  25929  itg2cnlem2  25930  itgss2  25981  itgeqa  25982  itgss3  25983  itgless  25985  ibladdlem  25988  itgaddlem1  25991  iblabslem  25996  itggt0  26012  itgcn  26013  ply1termlem  26369  plypf1  26378  plyaddlem1  26379  plymullem1  26380  coeeulem  26390  coeidlem  26403  coeid3  26406  coefv0  26414  coemulc  26421  dvply1  26454  vieta1lem2  26481  aaliou2  26512  logdmnrp  26815  regamcl  27234  lgam1  27237  gam1  27238  facgam  27239  chpub  27393  chebbnd1lem1  27642  numedglnl  29503  strlem1  32611  cycpmco2  33462  2sqr3minply  34179  sigaclfu2  34520  eulerpartlemb  34767  fineqvnttrclse  35545  setindregs  35551  mrsubcn  36019  dfon2lem6  36286  lindsadd  38292  ibladdnclem  38355  itgaddnclem1  38357  iblabsnclem  38362  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem8  38379  dvasin  38383  dvacos  38384  pridlc2  38751  pridlc3  38752  idomnnzgmulnz  42928  deg1gprod  42935  readvrec2  43150  readvrec  43151  fsuppssind  43353  irrapx1  43583  pellqrex  43634  qirropth  43663  setindtr  43779  kelac1  43818  flcidc  43925  arearect  43970  areaquad  43971  cantnfub  44076  mpct  45946  difmap  45951  difmapsn  45956  iccdificc  46283  fsumsupp0  46322  mccllem  46341  sumnnodd  46374  fprodcncf  46642  stoweidlem34  46776  stoweidlem44  46786  stirlinglem5  46820  fourierdlem62  46910  fouriersw  46973  elaa2lem  46975  etransclem44  47020  sge0iunmptlemfi  47155  sge0fodjrnlem  47158  meadjiunlem  47207  isomenndlem  47272  hsphoidmvle2  47327  hsphoidmvle  47328  hspdifhsp  47358  hspmbllem2  47369  ovnsubadd2lem  47387  ovolval4lem1  47391  preimagelt  47441  preimalegt  47442  tannpoly  47655