Theorem eldifn 4079

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ∖ cdif 3894

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900

This theorem is referenced by:  elndif  4080  disjel  4404  tz7.7  6332  partfun  6628  funiunfv  7182  tfi  7783  peano5  7823  resf1extb  7864  frrlem11  8226  frrlem12  8227  frrlem14  8229  tz7.48-2  8361  tz7.49  8364  oaf1o  8478  undifixp  8858  domdifsn  8973  isinf  9149  ordtypelem7  9410  unxpwdom2  9474  inf3lem3  9520  infdifsn  9547  cantnfp1lem1  9568  cantnfp1lem3  9570  cantnflem1d  9578  setind  9637  fin23lem30  10233  domtriomlem  10333  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  ttukeylem7  10406  konigthlem  10459  fpwwe2lem12  10533  fpwwe2  10534  hashf1lem1  14362  rlimrecl  15487  sumrblem  15618  fsumcvg  15619  summolem2a  15622  fsumss  15632  sumss2  15633  binomlem  15736  isumltss  15755  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  fprodss  15855  fprodsplit  15873  fprodmodd  15904  sumodd  16299  prmreclem2  16829  prmreclem5  16832  ramub1lem1  16938  chnccat  18532  efgs1b  19648  gsumzsplit  19839  gsum2d  19884  gsum2d2lem  19885  dmdprdsplitlem  19951  pgpfac1lem1  19988  irredrmul  20345  lbsextlem2  21096  lbsextlem4  21098  cnsubrg  21364  psrlidm  21899  mplcoe1  21972  mplcoe5  21975  evlslem3  22015  maducoeval2  22555  madugsum  22558  elcls  22988  isclo  23002  ptbasfi  23496  ptopn2  23499  xkopt  23570  kqdisj  23647  fin1aufil  23847  ptcmplem4  23970  opnsubg  24023  tsmssplit  24067  zcld  24729  recld2  24730  reconnlem1  24742  ioombl1lem4  25489  i1fima2sn  25608  itg1val2  25612  i1f0  25615  itg1addlem4  25627  mbfi1flim  25651  itg2splitlem  25676  itg2split  25677  itg2cnlem1  25689  itg2cnlem2  25690  itgss2  25741  itgeqa  25742  itgss3  25743  itgless  25745  ibladdlem  25748  itgaddlem1  25751  iblabslem  25756  itggt0  25772  itgcn  25773  ply1termlem  26135  plypf1  26144  plyaddlem1  26145  plymullem1  26146  coeeulem  26156  coeidlem  26169  coeid3  26172  coefv0  26180  coemulc  26187  dvply1  26218  vieta1lem2  26246  aaliou2  26275  logdmnrp  26577  regamcl  26998  lgam1  27001  gam1  27002  facgam  27003  chpub  27158  chebbnd1lem1  27407  numedglnl  29122  strlem1  32230  indval2  32835  ind0  32839  cycpmco2  33102  2sqr3minply  33793  sigaclfu2  34134  eulerpartlemb  34381  setindregs  35128  fineqvnttrclse  35144  mrsubcn  35563  dfon2lem6  35830  lindsadd  37663  ibladdnclem  37726  itgaddnclem1  37728  iblabsnclem  37733  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem8  37750  dvasin  37754  dvacos  37755  pridlc2  38122  pridlc3  38123  idomnnzgmulnz  42236  deg1gprod  42243  readvrec2  42464  readvrec  42465  selvvvval  42688  fsuppssind  42696  irrapx1  42931  pellqrex  42982  qirropth  43011  setindtr  43127  kelac1  43166  flcidc  43273  arearect  43318  areaquad  43319  cantnfub  43424  mpct  45308  difmap  45314  difmapsn  45319  iccdificc  45649  fsumsupp0  45688  mccllem  45707  sumnnodd  45740  fprodcncf  46008  stoweidlem34  46142  stoweidlem44  46152  stirlinglem5  46186  fourierdlem62  46276  fouriersw  46339  elaa2lem  46341  etransclem44  46386  sge0iunmptlemfi  46521  sge0fodjrnlem  46524  meadjiunlem  46573  isomenndlem  46638  hsphoidmvle2  46693  hsphoidmvle  46694  hspdifhsp  46724  hspmbllem2  46735  ovnsubadd2lem  46753  ovolval4lem1  46757  preimagelt  46807  preimalegt  46808  tannpoly  47000