Theorem eldifn 4081

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ∖ cdif 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901

This theorem is referenced by:  elndif  4082  disjel  4406  tz7.7  6337  partfun  6633  funiunfv  7188  tfi  7789  peano5  7829  resf1extb  7870  frrlem11  8232  frrlem12  8233  frrlem14  8235  tz7.48-2  8367  tz7.49  8370  oaf1o  8484  undifixp  8864  domdifsn  8980  isinf  9156  ordtypelem7  9417  unxpwdom2  9481  inf3lem3  9527  infdifsn  9554  cantnfp1lem1  9575  cantnfp1lem3  9577  cantnflem1d  9585  setind  9644  fin23lem30  10240  domtriomlem  10340  axdc3lem4  10351  axdc4lem  10353  axcclem  10355  ttukeylem7  10413  konigthlem  10466  fpwwe2lem12  10540  fpwwe2  10541  hashf1lem1  14364  rlimrecl  15489  sumrblem  15620  fsumcvg  15621  summolem2a  15624  fsumss  15634  sumss2  15635  binomlem  15738  isumltss  15757  prodrblem  15838  fprodcvg  15839  prodmolem2a  15843  fprodss  15857  fprodsplit  15875  fprodmodd  15906  sumodd  16301  prmreclem2  16831  prmreclem5  16834  ramub1lem1  16940  chnccat  18534  efgs1b  19650  gsumzsplit  19841  gsum2d  19886  gsum2d2lem  19887  dmdprdsplitlem  19953  pgpfac1lem1  19990  irredrmul  20347  lbsextlem2  21098  lbsextlem4  21100  cnsubrg  21366  psrlidm  21900  mplcoe1  21973  mplcoe5  21976  evlslem3  22016  maducoeval2  22556  madugsum  22559  elcls  22989  isclo  23003  ptbasfi  23497  ptopn2  23500  xkopt  23571  kqdisj  23648  fin1aufil  23848  ptcmplem4  23971  opnsubg  24024  tsmssplit  24068  zcld  24730  recld2  24731  reconnlem1  24743  ioombl1lem4  25490  i1fima2sn  25609  itg1val2  25613  i1f0  25616  itg1addlem4  25628  mbfi1flim  25652  itg2splitlem  25677  itg2split  25678  itg2cnlem1  25690  itg2cnlem2  25691  itgss2  25742  itgeqa  25743  itgss3  25744  itgless  25746  ibladdlem  25749  itgaddlem1  25752  iblabslem  25757  itggt0  25773  itgcn  25774  ply1termlem  26136  plypf1  26145  plyaddlem1  26146  plymullem1  26147  coeeulem  26157  coeidlem  26170  coeid3  26173  coefv0  26181  coemulc  26188  dvply1  26219  vieta1lem2  26247  aaliou2  26276  logdmnrp  26578  regamcl  26999  lgam1  27002  gam1  27003  facgam  27004  chpub  27159  chebbnd1lem1  27408  numedglnl  29124  strlem1  32232  indval2  32840  ind0  32844  cycpmco2  33109  2sqr3minply  33814  sigaclfu2  34155  eulerpartlemb  34402  setindregs  35149  fineqvnttrclse  35165  mrsubcn  35584  dfon2lem6  35851  lindsadd  37673  ibladdnclem  37736  itgaddnclem1  37738  iblabsnclem  37743  ftc1anclem5  37757  ftc1anclem6  37758  ftc1anclem8  37760  dvasin  37764  dvacos  37765  pridlc2  38132  pridlc3  38133  idomnnzgmulnz  42246  deg1gprod  42253  readvrec2  42479  readvrec  42480  selvvvval  42703  fsuppssind  42711  irrapx1  42945  pellqrex  42996  qirropth  43025  setindtr  43141  kelac1  43180  flcidc  43287  arearect  43332  areaquad  43333  cantnfub  43438  mpct  45322  difmap  45328  difmapsn  45333  iccdificc  45663  fsumsupp0  45702  mccllem  45721  sumnnodd  45754  fprodcncf  46022  stoweidlem34  46156  stoweidlem44  46166  stirlinglem5  46200  fourierdlem62  46290  fouriersw  46353  elaa2lem  46355  etransclem44  46400  sge0iunmptlemfi  46535  sge0fodjrnlem  46538  meadjiunlem  46587  isomenndlem  46652  hsphoidmvle2  46707  hsphoidmvle  46708  hspdifhsp  46738  hspmbllem2  46749  ovnsubadd2lem  46767  ovolval4lem1  46771  preimagelt  46821  preimalegt  46822  tannpoly  47014