Theorem eldifn 4079

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  elndif  4080  disjel  4410  tz7.7  6385  partfun  6682  funiunfv  7248  tfi  7855  peano5  7896  resf1extb  7937  frrlem11  8300  frrlem12  8301  frrlem14  8303  tz7.48-2  8438  tz7.49  8441  oaf1o  8557  undifixp  8948  domdifsn  9065  isinf  9242  ordtypelem7  9503  unxpwdom2  9567  inf3lem3  9616  infdifsn  9643  cantnfp1lem1  9664  cantnfp1lem3  9666  cantnflem1d  9674  setind  9733  fin23lem30  10369  domtriomlem  10469  axdc3lem4  10480  axdc4lem  10482  axcclem  10484  ttukeylem7  10542  konigthlem  10602  fpwwe2lem12  10676  fpwwe2  10677  indval2  12272  ind0  12277  hashf1lem1  14545  rlimrecl  15692  sumrblem  15822  fsumcvg  15823  summolem2a  15826  fsumss  15836  sumss2  15837  binomlem  15943  isumltss  15962  prodrblem  16041  fprodcvg  16042  prodmolem2a  16046  fprodss  16060  fprodsplit  16078  fprodmodd  16109  sumodd  16503  prmreclem2  17034  prmreclem5  17037  ramub1lem1  17143  chnccat  18739  efgs1b  19889  gsumzsplit  20080  gsum2d  20125  gsum2d2lem  20126  dmdprdsplitlem  20192  pgpfac1lem1  20229  irredrmul  20596  lbsextlem2  21376  lbsextlem4  21378  prmidlc2  21569  cmprmidlmcl  21570  cnsubrg  21672  psrlidm  22208  mplcoe1  22285  mplcoe5  22288  evlslem3  22328  selvvvval  22390  maducoeval2  22894  madugsum  22897  elcls  23330  isclo  23344  ptbasfi  23839  ptopn2  23842  xkopt  23913  kqdisj  23990  fin1aufil  24190  ptcmplem4  24313  opnsubg  24366  tsmssplit  24410  zcld  25072  recld2  25073  reconnlem1  25085  ioombl1lem4  25821  i1fima2sn  25940  itg1val2  25944  i1f0  25947  itg1addlem4  25959  mbfi1flim  25983  itg2splitlem  26008  itg2split  26009  itg2cnlem1  26021  itg2cnlem2  26022  itgss2  26072  itgeqa  26073  itgss3  26074  itgless  26076  ibladdlem  26079  itgaddlem1  26082  iblabslem  26087  itggt0  26103  itgcn  26104  ply1termlem  26460  plypf1  26470  plyaddlem1  26471  plymullem1  26472  coeeulem  26482  coeidlem  26495  coeid3  26498  coefv0  26506  coemulc  26513  dvply1  26546  vieta1lem2  26575  aaliou2  26608  logdmnrp  26910  regamcl  27329  lgam1  27332  gam1  27333  facgam  27334  chpub  27488  chebbnd1lem1  27737  numedglnl  29633  strlem1  32763  cycpmco2  33605  2sqr3minply  34323  sigaclfu2  34664  eulerpartlemb  34912  fineqvnttrclse  35693  setindregs  35699  mrsubcn  36181  dfon2lem6  36448  lindsadd  38432  ibladdnclem  38490  itgaddnclem1  38492  iblabsnclem  38497  ftc1anclem5  38511  ftc1anclem6  38512  ftc1anclem8  38514  dvasin  38518  dvacos  38519  pridlc2  38887  pridlc3  38888  idomnnzgmulnz  43064  deg1gprod  43071  readvrec2  43301  readvrec  43302  fsuppssind  43504  irrapx1  43734  pellqrex  43785  qirropth  43814  setindtr  43930  kelac1  43969  flcidc  44076  arearect  44121  areaquad  44122  cantnfub  44227  mpct  46097  difmap  46102  difmapsn  46107  iccdificc  46434  fsumsupp0  46473  mccllem  46492  sumnnodd  46525  fprodcncf  46793  stoweidlem34  46927  stoweidlem44  46937  stirlinglem5  46971  fourierdlem62  47061  fouriersw  47124  elaa2lem  47126  etransclem44  47171  sge0iunmptlemfi  47306  sge0fodjrnlem  47309  meadjiunlem  47358  isomenndlem  47423  hsphoidmvle2  47478  hsphoidmvle  47479  hspdifhsp  47509  hspmbllem2  47520  ovnsubadd2lem  47538  ovolval4lem1  47542  preimagelt  47592  preimalegt  47593  tannpoly  47823  tmachlem-tpopen  47834