Theorem eldifn 4092

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-dif 3914

This theorem is referenced by:  elndif  4093  disjel  4421  tz7.7  6387  partfun  6683  funiunfv  7247  tfi  7849  peano5  7890  resf1extb  7931  frrlem11  8293  frrlem12  8294  frrlem14  8296  tz7.48-2  8429  tz7.49  8432  oaf1o  8548  undifixp  8932  domdifsn  9048  isinf  9225  ordtypelem7  9486  unxpwdom2  9550  inf3lem3  9599  infdifsn  9626  cantnfp1lem1  9647  cantnfp1lem3  9649  cantnflem1d  9657  setind  9716  fin23lem30  10326  domtriomlem  10426  axdc3lem4  10437  axdc4lem  10439  axcclem  10441  ttukeylem7  10499  konigthlem  10553  fpwwe2lem12  10627  fpwwe2  10628  indval2  12223  ind0  12228  hashf1lem1  14492  rlimrecl  15631  sumrblem  15762  fsumcvg  15763  summolem2a  15766  fsumss  15776  sumss2  15777  binomlem  15883  isumltss  15902  prodrblem  15983  fprodcvg  15984  prodmolem2a  15988  fprodss  16002  fprodsplit  16020  fprodmodd  16051  sumodd  16446  prmreclem2  16977  prmreclem5  16980  ramub1lem1  17086  chnccat  18682  efgs1b  19806  gsumzsplit  19997  gsum2d  20042  gsum2d2lem  20043  dmdprdsplitlem  20109  pgpfac1lem1  20146  irredrmul  20509  lbsextlem2  21261  lbsextlem4  21263  cnsubrg  21546  psrlidm  22080  mplcoe1  22157  mplcoe5  22160  evlslem3  22200  selvvvval  22262  maducoeval2  22766  madugsum  22769  elcls  23199  isclo  23213  ptbasfi  23707  ptopn2  23710  xkopt  23781  kqdisj  23858  fin1aufil  24058  ptcmplem4  24181  opnsubg  24234  tsmssplit  24278  zcld  24940  recld2  24941  reconnlem1  24953  ioombl1lem4  25689  i1fima2sn  25808  itg1val2  25812  i1f0  25815  itg1addlem4  25827  mbfi1flim  25851  itg2splitlem  25876  itg2split  25877  itg2cnlem1  25889  itg2cnlem2  25890  itgss2  25941  itgeqa  25942  itgss3  25943  itgless  25945  ibladdlem  25948  itgaddlem1  25951  iblabslem  25956  itggt0  25972  itgcn  25973  ply1termlem  26329  plypf1  26338  plyaddlem1  26339  plymullem1  26340  coeeulem  26350  coeidlem  26363  coeid3  26366  coefv0  26374  coemulc  26381  dvply1  26414  vieta1lem2  26441  aaliou2  26470  logdmnrp  26772  regamcl  27191  lgam1  27194  gam1  27195  facgam  27196  chpub  27350  chebbnd1lem1  27599  numedglnl  29435  strlem1  32543  cycpmco2  33394  2sqr3minply  34115  sigaclfu2  34456  eulerpartlemb  34703  fineqvnttrclse  35470  setindregs  35476  mrsubcn  35944  dfon2lem6  36211  lindsadd  38187  ibladdnclem  38250  itgaddnclem1  38252  iblabsnclem  38257  ftc1anclem5  38271  ftc1anclem6  38272  ftc1anclem8  38274  dvasin  38278  dvacos  38279  pridlc2  38646  pridlc3  38647  idomnnzgmulnz  42825  deg1gprod  42832  readvrec2  43047  readvrec  43048  fsuppssind  43252  irrapx1  43482  pellqrex  43533  qirropth  43562  setindtr  43678  kelac1  43717  flcidc  43824  arearect  43869  areaquad  43870  cantnfub  43975  mpct  45845  difmap  45850  difmapsn  45855  iccdificc  46182  fsumsupp0  46221  mccllem  46240  sumnnodd  46273  fprodcncf  46541  stoweidlem34  46675  stoweidlem44  46685  stirlinglem5  46719  fourierdlem62  46809  fouriersw  46872  elaa2lem  46874  etransclem44  46919  sge0iunmptlemfi  47054  sge0fodjrnlem  47057  meadjiunlem  47106  isomenndlem  47171  hsphoidmvle2  47226  hsphoidmvle  47227  hspdifhsp  47257  hspmbllem2  47268  ovnsubadd2lem  47286  ovolval4lem1  47290  preimagelt  47340  preimalegt  47341  tannpoly  47551