Theorem eldifn 4155

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  elndif  4156  disjel  4480  tz7.7  6421  partfun  6727  funiunfv  7285  tfi  7890  peano5  7932  peano5OLD  7933  frrlem11  8337  frrlem12  8338  frrlem14  8340  wfrlem10OLD  8374  wfrlem13OLD  8377  wfrlem16OLD  8380  tz7.48-2  8498  tz7.49  8501  oaf1o  8619  undifixp  8992  domdifsn  9120  isinf  9323  isinfOLD  9324  ordtypelem7  9593  unxpwdom2  9657  inf3lem3  9699  infdifsn  9726  cantnfp1lem1  9747  cantnfp1lem3  9749  cantnflem1d  9757  setind  9803  fin23lem30  10411  domtriomlem  10511  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  ttukeylem7  10584  konigthlem  10637  fpwwe2lem12  10711  fpwwe2  10712  hashf1lem1  14504  rlimrecl  15626  sumrblem  15759  fsumcvg  15760  summolem2a  15763  fsumss  15773  sumss2  15774  binomlem  15877  isumltss  15896  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  fprodss  15996  fprodsplit  16014  fprodmodd  16045  sumodd  16436  prmreclem2  16964  prmreclem5  16967  ramub1lem1  17073  efgs1b  19778  gsumzsplit  19969  gsum2d  20014  gsum2d2lem  20015  dmdprdsplitlem  20081  pgpfac1lem1  20118  irredrmul  20453  lbsextlem2  21184  lbsextlem4  21186  cnsubrg  21468  psrlidm  22005  mplcoe1  22078  mplcoe5  22081  evlslem3  22127  maducoeval2  22667  madugsum  22670  elcls  23102  isclo  23116  ptbasfi  23610  ptopn2  23613  xkopt  23684  kqdisj  23761  fin1aufil  23961  ptcmplem4  24084  opnsubg  24137  tsmssplit  24181  zcld  24854  recld2  24855  reconnlem1  24867  ioombl1lem4  25615  i1fima2sn  25734  itg1val2  25738  i1f0  25741  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1flim  25778  itg2splitlem  25803  itg2split  25804  itg2cnlem1  25816  itg2cnlem2  25817  itgss2  25868  itgeqa  25869  itgss3  25870  itgless  25872  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  itggt0  25899  itgcn  25900  ply1termlem  26262  plypf1  26271  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeidlem  26296  coeid3  26299  coefv0  26307  coemulc  26314  dvply1  26343  vieta1lem2  26371  aaliou2  26400  logdmnrp  26701  regamcl  27122  lgam1  27125  gam1  27126  facgam  27127  chpub  27282  chebbnd1lem1  27531  numedglnl  29179  strlem1  32282  cycpmco2  33126  2sqr3minply  33738  indval2  33978  ind0  33982  sigaclfu2  34085  eulerpartlemb  34333  mrsubcn  35487  dfon2lem6  35752  lindsadd  37573  ibladdnclem  37636  itgaddnclem1  37638  iblabsnclem  37643  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem8  37660  dvasin  37664  dvacos  37665  pridlc2  38032  pridlc3  38033  idomnnzgmulnz  42090  deg1gprod  42097  selvvvval  42540  fsuppssind  42548  irrapx1  42784  pellqrex  42835  qirropth  42864  setindtr  42981  kelac1  43020  flcidc  43131  arearect  43176  areaquad  43177  cantnfub  43283  mpct  45108  difmap  45114  difmapsn  45119  iccdificc  45457  fsumsupp0  45499  mccllem  45518  sumnnodd  45551  fprodcncf  45821  stoweidlem34  45955  stoweidlem44  45965  stirlinglem5  45999  fourierdlem62  46089  fouriersw  46152  elaa2lem  46154  etransclem44  46199  sge0iunmptlemfi  46334  sge0fodjrnlem  46337  meadjiunlem  46386  isomenndlem  46451  hsphoidmvle2  46506  hsphoidmvle  46507  hspdifhsp  46537  hspmbllem2  46548  ovnsubadd2lem  46566  ovolval4lem1  46570  preimagelt  46620  preimalegt  46621