Theorem eldifn 4085

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

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

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 3443  df-dif 3905

This theorem is referenced by:  elndif  4086  disjel  4410  tz7.7  6344  partfun  6640  funiunfv  7196  tfi  7797  peano5  7837  resf1extb  7878  frrlem11  8240  frrlem12  8241  frrlem14  8243  tz7.48-2  8375  tz7.49  8378  oaf1o  8492  undifixp  8876  domdifsn  8992  isinf  9169  ordtypelem7  9433  unxpwdom2  9497  inf3lem3  9543  infdifsn  9570  cantnfp1lem1  9591  cantnfp1lem3  9593  cantnflem1d  9601  setind  9660  fin23lem30  10256  domtriomlem  10356  axdc3lem4  10367  axdc4lem  10369  axcclem  10371  ttukeylem7  10429  konigthlem  10483  fpwwe2lem12  10557  fpwwe2  10558  hashf1lem1  14382  rlimrecl  15507  sumrblem  15638  fsumcvg  15639  summolem2a  15642  fsumss  15652  sumss2  15653  binomlem  15756  isumltss  15775  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  fprodss  15875  fprodsplit  15893  fprodmodd  15924  sumodd  16319  prmreclem2  16849  prmreclem5  16852  ramub1lem1  16958  chnccat  18553  efgs1b  19669  gsumzsplit  19860  gsum2d  19905  gsum2d2lem  19906  dmdprdsplitlem  19972  pgpfac1lem1  20009  irredrmul  20367  lbsextlem2  21118  lbsextlem4  21120  cnsubrg  21386  psrlidm  21921  mplcoe1  21996  mplcoe5  21999  evlslem3  22039  maducoeval2  22588  madugsum  22591  elcls  23021  isclo  23035  ptbasfi  23529  ptopn2  23532  xkopt  23603  kqdisj  23680  fin1aufil  23880  ptcmplem4  24003  opnsubg  24056  tsmssplit  24100  zcld  24762  recld2  24763  reconnlem1  24775  ioombl1lem4  25522  i1fima2sn  25641  itg1val2  25645  i1f0  25648  itg1addlem4  25660  mbfi1flim  25684  itg2splitlem  25709  itg2split  25710  itg2cnlem1  25722  itg2cnlem2  25723  itgss2  25774  itgeqa  25775  itgss3  25776  itgless  25778  ibladdlem  25781  itgaddlem1  25784  iblabslem  25789  itggt0  25805  itgcn  25806  ply1termlem  26168  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  coeid3  26205  coefv0  26213  coemulc  26220  dvply1  26251  vieta1lem2  26279  aaliou2  26308  logdmnrp  26610  regamcl  27031  lgam1  27034  gam1  27035  facgam  27036  chpub  27191  chebbnd1lem1  27440  numedglnl  29221  strlem1  32329  indval2  32935  ind0  32939  cycpmco2  33217  2sqr3minply  33939  sigaclfu2  34280  eulerpartlemb  34527  fineqvnttrclse  35282  setindregs  35288  mrsubcn  35715  dfon2lem6  35982  lindsadd  37816  ibladdnclem  37879  itgaddnclem1  37881  iblabsnclem  37886  ftc1anclem5  37900  ftc1anclem6  37901  ftc1anclem8  37903  dvasin  37907  dvacos  37908  pridlc2  38275  pridlc3  38276  idomnnzgmulnz  42455  deg1gprod  42462  readvrec2  42683  readvrec  42684  selvvvval  42895  fsuppssind  42903  irrapx1  43137  pellqrex  43188  qirropth  43217  setindtr  43333  kelac1  43372  flcidc  43479  arearect  43524  areaquad  43525  cantnfub  43630  mpct  45512  difmap  45518  difmapsn  45523  iccdificc  45852  fsumsupp0  45891  mccllem  45910  sumnnodd  45943  fprodcncf  46211  stoweidlem34  46345  stoweidlem44  46355  stirlinglem5  46389  fourierdlem62  46479  fouriersw  46542  elaa2lem  46544  etransclem44  46589  sge0iunmptlemfi  46724  sge0fodjrnlem  46727  meadjiunlem  46776  isomenndlem  46841  hsphoidmvle2  46896  hsphoidmvle  46897  hspdifhsp  46927  hspmbllem2  46938  ovnsubadd2lem  46956  ovolval4lem1  46960  preimagelt  47010  preimalegt  47011  tannpoly  47203