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  28435  strlem1  31534  cycpmco2  32323  indval2  33043  ind0  33047  sigaclfu2  33150  eulerpartlemb  33398  mrsubcn  34541  dfon2lem6  34791  lindsadd  36529  ibladdnclem  36592  itgaddnclem1  36594  iblabsnclem  36599  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anclem8  36616  dvasin  36620  dvacos  36621  pridlc2  36988  pridlc3  36989  selvvvval  41205  fsuppssind  41213  irrapx1  41614  pellqrex  41665  qirropth  41694  setindtr  41811  kelac1  41853  flcidc  41964  arearect  42012  areaquad  42013  cantnfub  42119  mpct  43948  difmap  43954  difmapsn  43959  iccdificc  44300  fsumsupp0  44342  mccllem  44361  sumnnodd  44394  fprodcncf  44664  stoweidlem34  44798  stoweidlem44  44808  stirlinglem5  44842  fourierdlem62  44932  fouriersw  44995  elaa2lem  44997  etransclem44  45042  sge0iunmptlemfi  45177  sge0fodjrnlem  45180  meadjiunlem  45229  isomenndlem  45294  hsphoidmvle2  45349  hsphoidmvle  45350  hspdifhsp  45380  hspmbllem2  45391  ovnsubadd2lem  45409  ovolval4lem1  45413  preimagelt  45463  preimalegt  45464