Theorem eldifn 4128

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952

This theorem is referenced by:  elndif  4129  disjel  4457  tz7.7  6391  partfun  6698  funiunfv  7247  tfi  7842  peano5  7884  peano5OLD  7885  frrlem11  8281  frrlem12  8282  frrlem14  8284  wfrlem10OLD  8318  wfrlem13OLD  8321  wfrlem16OLD  8324  tz7.48-2  8442  tz7.49  8445  oaf1o  8563  undifixp  8928  domdifsn  9054  isinf  9260  isinfOLD  9261  ordtypelem7  9519  unxpwdom2  9583  inf3lem3  9625  infdifsn  9652  cantnfp1lem1  9673  cantnfp1lem3  9675  cantnflem1d  9683  setind  9729  fin23lem30  10337  domtriomlem  10437  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  ttukeylem7  10510  konigthlem  10563  fpwwe2lem12  10637  fpwwe2  10638  hashf1lem1  14415  hashf1lem1OLD  14416  rlimrecl  15524  sumrblem  15657  fsumcvg  15658  summolem2a  15661  fsumss  15671  sumss2  15672  binomlem  15775  isumltss  15794  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  fprodss  15892  fprodsplit  15910  fprodmodd  15941  sumodd  16331  prmreclem2  16850  prmreclem5  16853  ramub1lem1  16959  efgs1b  19604  gsumzsplit  19795  gsum2d  19840  gsum2d2lem  19841  dmdprdsplitlem  19907  pgpfac1lem1  19944  irredrmul  20241  lbsextlem2  20772  lbsextlem4  20774  cnsubrg  21005  psrlidm  21523  mplcoe1  21592  mplcoe5  21595  evlslem3  21643  maducoeval2  22142  madugsum  22145  elcls  22577  isclo  22591  ptbasfi  23085  ptopn2  23088  xkopt  23159  kqdisj  23236  fin1aufil  23436  ptcmplem4  23559  opnsubg  23612  tsmssplit  23656  zcld  24329  recld2  24330  reconnlem1  24342  ioombl1lem4  25078  i1fima2sn  25197  itg1val2  25201  i1f0  25204  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1flim  25241  itg2splitlem  25266  itg2split  25267  itg2cnlem1  25279  itg2cnlem2  25280  itgss2  25330  itgeqa  25331  itgss3  25332  itgless  25334  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  itggt0  25361  itgcn  25362  ply1termlem  25717  plypf1  25726  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  coeidlem  25751  coeid3  25754  coefv0  25762  coemulc  25769  dvply1  25797  vieta1lem2  25824  aaliou2  25853  logdmnrp  26149  regamcl  26565  lgam1  26568  gam1  26569  facgam  26570  chpub  26723  chebbnd1lem1  26972  numedglnl  28404  strlem1  31503  cycpmco2  32292  indval2  33012  ind0  33016  sigaclfu2  33119  eulerpartlemb  33367  mrsubcn  34510  dfon2lem6  34760  lindsadd  36481  ibladdnclem  36544  itgaddnclem1  36546  iblabsnclem  36551  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem8  36568  dvasin  36572  dvacos  36573  pridlc2  36940  pridlc3  36941  selvvvval  41157  fsuppssind  41165  irrapx1  41566  pellqrex  41617  qirropth  41646  setindtr  41763  kelac1  41805  flcidc  41916  arearect  41964  areaquad  41965  cantnfub  42071  mpct  43900  difmap  43906  difmapsn  43911  iccdificc  44252  fsumsupp0  44294  mccllem  44313  sumnnodd  44346  fprodcncf  44616  stoweidlem34  44750  stoweidlem44  44760  stirlinglem5  44794  fourierdlem62  44884  fouriersw  44947  elaa2lem  44949  etransclem44  44994  sge0iunmptlemfi  45129  sge0fodjrnlem  45132  meadjiunlem  45181  isomenndlem  45246  hsphoidmvle2  45301  hsphoidmvle  45302  hspdifhsp  45332  hspmbllem2  45343  ovnsubadd2lem  45361  ovolval4lem1  45365  preimagelt  45415  preimalegt  45416