Theorem eldifn 4073

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893

This theorem is referenced by:  elndif  4074  disjel  4398  tz7.7  6345  partfun  6641  funiunfv  7198  tfi  7799  peano5  7839  resf1extb  7880  frrlem11  8241  frrlem12  8242  frrlem14  8244  tz7.48-2  8376  tz7.49  8379  oaf1o  8493  undifixp  8877  domdifsn  8993  isinf  9170  ordtypelem7  9434  unxpwdom2  9498  inf3lem3  9546  infdifsn  9573  cantnfp1lem1  9594  cantnfp1lem3  9596  cantnflem1d  9604  setind  9663  fin23lem30  10259  domtriomlem  10359  axdc3lem4  10370  axdc4lem  10372  axcclem  10374  ttukeylem7  10432  konigthlem  10486  fpwwe2lem12  10560  fpwwe2  10561  indval2  12159  ind0  12164  hashf1lem1  14412  rlimrecl  15537  sumrblem  15668  fsumcvg  15669  summolem2a  15672  fsumss  15682  sumss2  15683  binomlem  15789  isumltss  15808  prodrblem  15889  fprodcvg  15890  prodmolem2a  15894  fprodss  15908  fprodsplit  15926  fprodmodd  15957  sumodd  16352  prmreclem2  16883  prmreclem5  16886  ramub1lem1  16992  chnccat  18587  efgs1b  19706  gsumzsplit  19897  gsum2d  19942  gsum2d2lem  19943  dmdprdsplitlem  20009  pgpfac1lem1  20046  irredrmul  20402  lbsextlem2  21153  lbsextlem4  21155  cnsubrg  21421  psrlidm  21954  mplcoe1  22029  mplcoe5  22032  evlslem3  22072  maducoeval2  22619  madugsum  22622  elcls  23052  isclo  23066  ptbasfi  23560  ptopn2  23563  xkopt  23634  kqdisj  23711  fin1aufil  23911  ptcmplem4  24034  opnsubg  24087  tsmssplit  24131  zcld  24793  recld2  24794  reconnlem1  24806  ioombl1lem4  25542  i1fima2sn  25661  itg1val2  25665  i1f0  25668  itg1addlem4  25680  mbfi1flim  25704  itg2splitlem  25729  itg2split  25730  itg2cnlem1  25742  itg2cnlem2  25743  itgss2  25794  itgeqa  25795  itgss3  25796  itgless  25798  ibladdlem  25801  itgaddlem1  25804  iblabslem  25809  itggt0  25825  itgcn  25826  ply1termlem  26182  plypf1  26191  plyaddlem1  26192  plymullem1  26193  coeeulem  26203  coeidlem  26216  coeid3  26219  coefv0  26227  coemulc  26234  dvply1  26264  vieta1lem2  26292  aaliou2  26321  logdmnrp  26622  regamcl  27042  lgam1  27045  gam1  27046  facgam  27047  chpub  27201  chebbnd1lem1  27450  numedglnl  29231  strlem1  32340  cycpmco2  33213  2sqr3minply  33944  sigaclfu2  34285  eulerpartlemb  34532  fineqvnttrclse  35288  setindregs  35294  mrsubcn  35721  dfon2lem6  35988  lindsadd  37952  ibladdnclem  38015  itgaddnclem1  38017  iblabsnclem  38022  ftc1anclem5  38036  ftc1anclem6  38037  ftc1anclem8  38039  dvasin  38043  dvacos  38044  pridlc2  38411  pridlc3  38412  idomnnzgmulnz  42590  deg1gprod  42597  readvrec2  42811  readvrec  42812  selvvvval  43036  fsuppssind  43044  irrapx1  43278  pellqrex  43329  qirropth  43358  setindtr  43474  kelac1  43513  flcidc  43620  arearect  43665  areaquad  43666  cantnfub  43771  mpct  45652  difmap  45658  difmapsn  45663  iccdificc  45991  fsumsupp0  46030  mccllem  46049  sumnnodd  46082  fprodcncf  46350  stoweidlem34  46484  stoweidlem44  46494  stirlinglem5  46528  fourierdlem62  46618  fouriersw  46681  elaa2lem  46683  etransclem44  46728  sge0iunmptlemfi  46863  sge0fodjrnlem  46866  meadjiunlem  46915  isomenndlem  46980  hsphoidmvle2  47035  hsphoidmvle  47036  hspdifhsp  47066  hspmbllem2  47077  ovnsubadd2lem  47095  ovolval4lem1  47099  preimagelt  47149  preimalegt  47150  tannpoly  47354