Theorem eldifn 4072

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892

This theorem is referenced by:  elndif  4073  disjel  4397  tz7.7  6349  partfun  6645  funiunfv  7203  tfi  7804  peano5  7844  resf1extb  7885  frrlem11  8246  frrlem12  8247  frrlem14  8249  tz7.48-2  8381  tz7.49  8384  oaf1o  8498  undifixp  8882  domdifsn  8998  isinf  9175  ordtypelem7  9439  unxpwdom2  9503  inf3lem3  9551  infdifsn  9578  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem1d  9609  setind  9668  fin23lem30  10264  domtriomlem  10364  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  ttukeylem7  10437  konigthlem  10491  fpwwe2lem12  10565  fpwwe2  10566  indval2  12164  ind0  12169  hashf1lem1  14417  rlimrecl  15542  sumrblem  15673  fsumcvg  15674  summolem2a  15677  fsumss  15687  sumss2  15688  binomlem  15794  isumltss  15813  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  fprodss  15913  fprodsplit  15931  fprodmodd  15962  sumodd  16357  prmreclem2  16888  prmreclem5  16891  ramub1lem1  16997  chnccat  18592  efgs1b  19711  gsumzsplit  19902  gsum2d  19947  gsum2d2lem  19948  dmdprdsplitlem  20014  pgpfac1lem1  20051  irredrmul  20407  lbsextlem2  21157  lbsextlem4  21159  cnsubrg  21407  psrlidm  21940  mplcoe1  22015  mplcoe5  22018  evlslem3  22058  maducoeval2  22605  madugsum  22608  elcls  23038  isclo  23052  ptbasfi  23546  ptopn2  23549  xkopt  23620  kqdisj  23697  fin1aufil  23897  ptcmplem4  24020  opnsubg  24073  tsmssplit  24117  zcld  24779  recld2  24780  reconnlem1  24792  ioombl1lem4  25528  i1fima2sn  25647  itg1val2  25651  i1f0  25654  itg1addlem4  25666  mbfi1flim  25690  itg2splitlem  25715  itg2split  25716  itg2cnlem1  25728  itg2cnlem2  25729  itgss2  25780  itgeqa  25781  itgss3  25782  itgless  25784  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  itggt0  25811  itgcn  25812  ply1termlem  26168  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  coeid3  26205  coefv0  26213  coemulc  26220  dvply1  26250  vieta1lem2  26277  aaliou2  26306  logdmnrp  26605  regamcl  27024  lgam1  27027  gam1  27028  facgam  27029  chpub  27183  chebbnd1lem1  27432  numedglnl  29213  strlem1  32321  cycpmco2  33194  2sqr3minply  33924  sigaclfu2  34265  eulerpartlemb  34512  fineqvnttrclse  35268  setindregs  35274  mrsubcn  35701  dfon2lem6  35968  lindsadd  37934  ibladdnclem  37997  itgaddnclem1  37999  iblabsnclem  38004  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem8  38021  dvasin  38025  dvacos  38026  pridlc2  38393  pridlc3  38394  idomnnzgmulnz  42572  deg1gprod  42579  readvrec2  42793  readvrec  42794  selvvvval  43018  fsuppssind  43026  irrapx1  43256  pellqrex  43307  qirropth  43336  setindtr  43452  kelac1  43491  flcidc  43598  arearect  43643  areaquad  43644  cantnfub  43749  mpct  45630  difmap  45636  difmapsn  45641  iccdificc  45969  fsumsupp0  46008  mccllem  46027  sumnnodd  46060  fprodcncf  46328  stoweidlem34  46462  stoweidlem44  46472  stirlinglem5  46506  fourierdlem62  46596  fouriersw  46659  elaa2lem  46661  etransclem44  46706  sge0iunmptlemfi  46841  sge0fodjrnlem  46844  meadjiunlem  46893  isomenndlem  46958  hsphoidmvle2  47013  hsphoidmvle  47014  hspdifhsp  47044  hspmbllem2  47055  ovnsubadd2lem  47073  ovolval4lem1  47077  preimagelt  47127  preimalegt  47128  tannpoly  47338