Theorem eldifn 4091

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914

This theorem is referenced by:  elndif  4092  disjel  4416  tz7.7  6346  partfun  6647  funiunfv  7204  tfi  7809  peano5  7849  resf1extb  7890  frrlem11  8252  frrlem12  8253  frrlem14  8255  tz7.48-2  8387  tz7.49  8390  oaf1o  8504  undifixp  8884  domdifsn  9001  isinf  9183  isinfOLD  9184  ordtypelem7  9453  unxpwdom2  9517  inf3lem3  9559  infdifsn  9586  cantnfp1lem1  9607  cantnfp1lem3  9609  cantnflem1d  9617  setind  9663  fin23lem30  10271  domtriomlem  10371  axdc3lem4  10382  axdc4lem  10384  axcclem  10386  ttukeylem7  10444  konigthlem  10497  fpwwe2lem12  10571  fpwwe2  10572  hashf1lem1  14396  rlimrecl  15522  sumrblem  15653  fsumcvg  15654  summolem2a  15657  fsumss  15667  sumss2  15668  binomlem  15771  isumltss  15790  prodrblem  15871  fprodcvg  15872  prodmolem2a  15876  fprodss  15890  fprodsplit  15908  fprodmodd  15939  sumodd  16334  prmreclem2  16864  prmreclem5  16867  ramub1lem1  16973  efgs1b  19650  gsumzsplit  19841  gsum2d  19886  gsum2d2lem  19887  dmdprdsplitlem  19953  pgpfac1lem1  19990  irredrmul  20347  lbsextlem2  21101  lbsextlem4  21103  cnsubrg  21369  psrlidm  21904  mplcoe1  21977  mplcoe5  21980  evlslem3  22020  maducoeval2  22560  madugsum  22563  elcls  22993  isclo  23007  ptbasfi  23501  ptopn2  23504  xkopt  23575  kqdisj  23652  fin1aufil  23852  ptcmplem4  23975  opnsubg  24028  tsmssplit  24072  zcld  24735  recld2  24736  reconnlem1  24748  ioombl1lem4  25495  i1fima2sn  25614  itg1val2  25618  i1f0  25621  itg1addlem4  25633  mbfi1flim  25657  itg2splitlem  25682  itg2split  25683  itg2cnlem1  25695  itg2cnlem2  25696  itgss2  25747  itgeqa  25748  itgss3  25749  itgless  25751  ibladdlem  25754  itgaddlem1  25757  iblabslem  25762  itggt0  25778  itgcn  25779  ply1termlem  26141  plypf1  26150  plyaddlem1  26151  plymullem1  26152  coeeulem  26162  coeidlem  26175  coeid3  26178  coefv0  26186  coemulc  26193  dvply1  26224  vieta1lem2  26252  aaliou2  26281  logdmnrp  26583  regamcl  27004  lgam1  27007  gam1  27008  facgam  27009  chpub  27164  chebbnd1lem1  27413  numedglnl  29124  strlem1  32229  indval2  32827  ind0  32831  cycpmco2  33105  2sqr3minply  33763  sigaclfu2  34104  eulerpartlemb  34352  mrsubcn  35499  dfon2lem6  35769  lindsadd  37600  ibladdnclem  37663  itgaddnclem1  37665  iblabsnclem  37670  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem8  37687  dvasin  37691  dvacos  37692  pridlc2  38059  pridlc3  38060  idomnnzgmulnz  42114  deg1gprod  42121  readvrec2  42342  readvrec  42343  selvvvval  42566  fsuppssind  42574  irrapx1  42809  pellqrex  42860  qirropth  42889  setindtr  43006  kelac1  43045  flcidc  43152  arearect  43197  areaquad  43198  cantnfub  43303  mpct  45188  difmap  45194  difmapsn  45199  iccdificc  45530  fsumsupp0  45569  mccllem  45588  sumnnodd  45621  fprodcncf  45891  stoweidlem34  46025  stoweidlem44  46035  stirlinglem5  46069  fourierdlem62  46159  fouriersw  46222  elaa2lem  46224  etransclem44  46269  sge0iunmptlemfi  46404  sge0fodjrnlem  46407  meadjiunlem  46456  isomenndlem  46521  hsphoidmvle2  46576  hsphoidmvle  46577  hspdifhsp  46607  hspmbllem2  46618  ovnsubadd2lem  46636  ovolval4lem1  46640  preimagelt  46690  preimalegt  46691  tannpoly  46884