Theorem eldifn 4126

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3950

This theorem is referenced by:  elndif  4127  disjel  4455  tz7.7  6387  partfun  6694  funiunfv  7242  tfi  7837  peano5  7879  peano5OLD  7880  frrlem11  8276  frrlem12  8277  frrlem14  8279  wfrlem10OLD  8313  wfrlem13OLD  8316  wfrlem16OLD  8319  tz7.48-2  8437  tz7.49  8440  oaf1o  8559  undifixp  8924  domdifsn  9050  isinf  9256  isinfOLD  9257  ordtypelem7  9515  unxpwdom2  9579  inf3lem3  9621  infdifsn  9648  cantnfp1lem1  9669  cantnfp1lem3  9671  cantnflem1d  9679  setind  9725  fin23lem30  10333  domtriomlem  10433  axdc3lem4  10444  axdc4lem  10446  axcclem  10448  ttukeylem7  10506  konigthlem  10559  fpwwe2lem12  10633  fpwwe2  10634  hashf1lem1  14411  hashf1lem1OLD  14412  rlimrecl  15520  sumrblem  15653  fsumcvg  15654  summolem2a  15657  fsumss  15667  sumss2  15668  binomlem  15771  isumltss  15790  prodrblem  15869  fprodcvg  15870  prodmolem2a  15874  fprodss  15888  fprodsplit  15906  fprodmodd  15937  sumodd  16327  prmreclem2  16846  prmreclem5  16849  ramub1lem1  16955  efgs1b  19597  gsumzsplit  19787  gsum2d  19832  gsum2d2lem  19833  dmdprdsplitlem  19899  pgpfac1lem1  19936  irredrmul  20230  lbsextlem2  20760  lbsextlem4  20762  cnsubrg  20990  psrlidm  21505  mplcoe1  21574  mplcoe5  21577  evlslem3  21625  maducoeval2  22124  madugsum  22127  elcls  22559  isclo  22573  ptbasfi  23067  ptopn2  23070  xkopt  23141  kqdisj  23218  fin1aufil  23418  ptcmplem4  23541  opnsubg  23594  tsmssplit  23638  zcld  24311  recld2  24312  reconnlem1  24324  ioombl1lem4  25060  i1fima2sn  25179  itg1val2  25183  i1f0  25186  itg1addlem4  25198  itg1addlem4OLD  25199  mbfi1flim  25223  itg2splitlem  25248  itg2split  25249  itg2cnlem1  25261  itg2cnlem2  25262  itgss2  25312  itgeqa  25313  itgss3  25314  itgless  25316  ibladdlem  25319  itgaddlem1  25322  iblabslem  25327  itggt0  25343  itgcn  25344  ply1termlem  25699  plypf1  25708  plyaddlem1  25709  plymullem1  25710  coeeulem  25720  coeidlem  25733  coeid3  25736  coefv0  25744  coemulc  25751  dvply1  25779  vieta1lem2  25806  aaliou2  25835  logdmnrp  26131  regamcl  26545  lgam1  26548  gam1  26549  facgam  26550  chpub  26703  chebbnd1lem1  26952  numedglnl  28384  strlem1  31481  cycpmco2  32270  indval2  32950  ind0  32954  sigaclfu2  33057  eulerpartlemb  33305  mrsubcn  34448  dfon2lem6  34698  lindsadd  36419  ibladdnclem  36482  itgaddnclem1  36484  iblabsnclem  36489  ftc1anclem5  36503  ftc1anclem6  36504  ftc1anclem8  36506  dvasin  36510  dvacos  36511  pridlc2  36878  pridlc3  36879  selvvvval  41107  fsuppssind  41115  irrapx1  41499  pellqrex  41550  qirropth  41579  setindtr  41696  kelac1  41738  flcidc  41849  arearect  41897  areaquad  41898  cantnfub  42004  mpct  43833  difmap  43839  difmapsn  43844  iccdificc  44187  fsumsupp0  44229  mccllem  44248  sumnnodd  44281  fprodcncf  44551  stoweidlem34  44685  stoweidlem44  44695  stirlinglem5  44729  fourierdlem62  44819  fouriersw  44882  elaa2lem  44884  etransclem44  44929  sge0iunmptlemfi  45064  sge0fodjrnlem  45067  meadjiunlem  45116  isomenndlem  45181  hsphoidmvle2  45236  hsphoidmvle  45237  hspdifhsp  45267  hspmbllem2  45278  ovnsubadd2lem  45296  ovolval4lem1  45300  preimagelt  45350  preimalegt  45351