Theorem eldifn 4087

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2144   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-dif 3909

This theorem is referenced by:  elndif  4088  disjel  4413  tz7.7  6374  partfun  6670  funiunfv  7234  tfi  7835  peano5  7876  resf1extb  7917  frrlem11  8279  frrlem12  8280  frrlem14  8282  tz7.48-2  8415  tz7.49  8418  oaf1o  8534  undifixp  8918  domdifsn  9034  isinf  9211  ordtypelem7  9474  unxpwdom2  9538  inf3lem3  9587  infdifsn  9614  cantnfp1lem1  9635  cantnfp1lem3  9637  cantnflem1d  9645  setind  9704  fin23lem30  10301  domtriomlem  10401  axdc3lem4  10412  axdc4lem  10414  axcclem  10416  ttukeylem7  10474  konigthlem  10528  fpwwe2lem12  10602  fpwwe2  10603  indval2  12202  ind0  12207  hashf1lem1  14470  rlimrecl  15609  sumrblem  15740  fsumcvg  15741  summolem2a  15744  fsumss  15754  sumss2  15755  binomlem  15861  isumltss  15880  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  fprodss  15980  fprodsplit  15998  fprodmodd  16029  sumodd  16424  prmreclem2  16955  prmreclem5  16958  ramub1lem1  17064  chnccat  18660  efgs1b  19778  gsumzsplit  19969  gsum2d  20014  gsum2d2lem  20015  dmdprdsplitlem  20081  pgpfac1lem1  20118  irredrmul  20478  lbsextlem2  21231  lbsextlem4  21233  cnsubrg  21481  psrlidm  22015  mplcoe1  22092  mplcoe5  22095  evlslem3  22135  selvvvval  22197  maducoeval2  22702  madugsum  22705  elcls  23135  isclo  23149  ptbasfi  23643  ptopn2  23646  xkopt  23717  kqdisj  23794  fin1aufil  23994  ptcmplem4  24117  opnsubg  24170  tsmssplit  24214  zcld  24876  recld2  24877  reconnlem1  24889  ioombl1lem4  25625  i1fima2sn  25744  itg1val2  25748  i1f0  25751  itg1addlem4  25763  mbfi1flim  25787  itg2splitlem  25812  itg2split  25813  itg2cnlem1  25825  itg2cnlem2  25826  itgss2  25877  itgeqa  25878  itgss3  25879  itgless  25881  ibladdlem  25884  itgaddlem1  25887  iblabslem  25892  itggt0  25908  itgcn  25909  ply1termlem  26265  plypf1  26274  plyaddlem1  26275  plymullem1  26276  coeeulem  26286  coeidlem  26299  coeid3  26302  coefv0  26310  coemulc  26317  dvply1  26350  vieta1lem2  26377  aaliou2  26406  logdmnrp  26708  regamcl  27127  lgam1  27130  gam1  27131  facgam  27132  chpub  27286  chebbnd1lem1  27535  numedglnl  29347  strlem1  32455  cycpmco2  33315  2sqr3minply  34079  sigaclfu2  34420  eulerpartlemb  34667  fineqvnttrclse  35424  setindregs  35430  mrsubcn  35874  dfon2lem6  36141  lindsadd  38117  ibladdnclem  38180  itgaddnclem1  38182  iblabsnclem  38187  ftc1anclem5  38201  ftc1anclem6  38202  ftc1anclem8  38204  dvasin  38208  dvacos  38209  pridlc2  38576  pridlc3  38577  idomnnzgmulnz  42755  deg1gprod  42762  readvrec2  42975  readvrec  42976  fsuppssind  43180  irrapx1  43410  pellqrex  43461  qirropth  43490  setindtr  43606  kelac1  43645  flcidc  43752  arearect  43797  areaquad  43798  cantnfub  43903  mpct  45783  difmap  45788  difmapsn  45793  iccdificc  46120  fsumsupp0  46159  mccllem  46178  sumnnodd  46211  fprodcncf  46479  stoweidlem34  46613  stoweidlem44  46623  stirlinglem5  46657  fourierdlem62  46747  fouriersw  46810  elaa2lem  46812  etransclem44  46857  sge0iunmptlemfi  46992  sge0fodjrnlem  46995  meadjiunlem  47044  isomenndlem  47109  hsphoidmvle2  47164  hsphoidmvle  47165  hspdifhsp  47195  hspmbllem2  47206  ovnsubadd2lem  47224  ovolval4lem1  47228  preimagelt  47278  preimalegt  47279  tannpoly  47489