Theorem eldifn 4132

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954

This theorem is referenced by:  elndif  4133  disjel  4457  tz7.7  6410  partfun  6715  funiunfv  7268  tfi  7874  peano5  7915  resf1extb  7956  frrlem11  8321  frrlem12  8322  frrlem14  8324  wfrlem10OLD  8358  wfrlem13OLD  8361  wfrlem16OLD  8364  tz7.48-2  8482  tz7.49  8485  oaf1o  8601  undifixp  8974  domdifsn  9094  isinf  9296  isinfOLD  9297  ordtypelem7  9564  unxpwdom2  9628  inf3lem3  9670  infdifsn  9697  cantnfp1lem1  9718  cantnfp1lem3  9720  cantnflem1d  9728  setind  9774  fin23lem30  10382  domtriomlem  10482  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  ttukeylem7  10555  konigthlem  10608  fpwwe2lem12  10682  fpwwe2  10683  hashf1lem1  14494  rlimrecl  15616  sumrblem  15747  fsumcvg  15748  summolem2a  15751  fsumss  15761  sumss2  15762  binomlem  15865  isumltss  15884  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  fprodss  15984  fprodsplit  16002  fprodmodd  16033  sumodd  16425  prmreclem2  16955  prmreclem5  16958  ramub1lem1  17064  efgs1b  19754  gsumzsplit  19945  gsum2d  19990  gsum2d2lem  19991  dmdprdsplitlem  20057  pgpfac1lem1  20094  irredrmul  20427  lbsextlem2  21161  lbsextlem4  21163  cnsubrg  21445  psrlidm  21982  mplcoe1  22055  mplcoe5  22058  evlslem3  22104  maducoeval2  22646  madugsum  22649  elcls  23081  isclo  23095  ptbasfi  23589  ptopn2  23592  xkopt  23663  kqdisj  23740  fin1aufil  23940  ptcmplem4  24063  opnsubg  24116  tsmssplit  24160  zcld  24835  recld2  24836  reconnlem1  24848  ioombl1lem4  25596  i1fima2sn  25715  itg1val2  25719  i1f0  25722  itg1addlem4  25734  mbfi1flim  25758  itg2splitlem  25783  itg2split  25784  itg2cnlem1  25796  itg2cnlem2  25797  itgss2  25848  itgeqa  25849  itgss3  25850  itgless  25852  ibladdlem  25855  itgaddlem1  25858  iblabslem  25863  itggt0  25879  itgcn  25880  ply1termlem  26242  plypf1  26251  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeidlem  26276  coeid3  26279  coefv0  26287  coemulc  26294  dvply1  26325  vieta1lem2  26353  aaliou2  26382  logdmnrp  26683  regamcl  27104  lgam1  27107  gam1  27108  facgam  27109  chpub  27264  chebbnd1lem1  27513  numedglnl  29161  strlem1  32269  indval2  32839  ind0  32843  cycpmco2  33153  2sqr3minply  33791  sigaclfu2  34122  eulerpartlemb  34370  mrsubcn  35524  dfon2lem6  35789  lindsadd  37620  ibladdnclem  37683  itgaddnclem1  37685  iblabsnclem  37690  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem8  37707  dvasin  37711  dvacos  37712  pridlc2  38079  pridlc3  38080  idomnnzgmulnz  42134  deg1gprod  42141  readvrec2  42391  readvrec  42392  selvvvval  42595  fsuppssind  42603  irrapx1  42839  pellqrex  42890  qirropth  42919  setindtr  43036  kelac1  43075  flcidc  43182  arearect  43227  areaquad  43228  cantnfub  43334  mpct  45206  difmap  45212  difmapsn  45217  iccdificc  45552  fsumsupp0  45593  mccllem  45612  sumnnodd  45645  fprodcncf  45915  stoweidlem34  46049  stoweidlem44  46059  stirlinglem5  46093  fourierdlem62  46183  fouriersw  46246  elaa2lem  46248  etransclem44  46293  sge0iunmptlemfi  46428  sge0fodjrnlem  46431  meadjiunlem  46480  isomenndlem  46545  hsphoidmvle2  46600  hsphoidmvle  46601  hspdifhsp  46631  hspmbllem2  46642  ovnsubadd2lem  46660  ovolval4lem1  46664  preimagelt  46714  preimalegt  46715