Theorem eldifn 4141

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965

This theorem is referenced by:  elndif  4142  disjel  4462  tz7.7  6411  partfun  6715  funiunfv  7267  tfi  7873  peano5  7915  frrlem11  8319  frrlem12  8320  frrlem14  8322  wfrlem10OLD  8356  wfrlem13OLD  8359  wfrlem16OLD  8362  tz7.48-2  8480  tz7.49  8483  oaf1o  8599  undifixp  8972  domdifsn  9092  isinf  9293  isinfOLD  9294  ordtypelem7  9561  unxpwdom2  9625  inf3lem3  9667  infdifsn  9694  cantnfp1lem1  9715  cantnfp1lem3  9717  cantnflem1d  9725  setind  9771  fin23lem30  10379  domtriomlem  10479  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  ttukeylem7  10552  konigthlem  10605  fpwwe2lem12  10679  fpwwe2  10680  hashf1lem1  14490  rlimrecl  15612  sumrblem  15743  fsumcvg  15744  summolem2a  15747  fsumss  15757  sumss2  15758  binomlem  15861  isumltss  15880  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  fprodss  15980  fprodsplit  15998  fprodmodd  16029  sumodd  16421  prmreclem2  16950  prmreclem5  16953  ramub1lem1  17059  efgs1b  19768  gsumzsplit  19959  gsum2d  20004  gsum2d2lem  20005  dmdprdsplitlem  20071  pgpfac1lem1  20108  irredrmul  20443  lbsextlem2  21178  lbsextlem4  21180  cnsubrg  21462  psrlidm  21999  mplcoe1  22072  mplcoe5  22075  evlslem3  22121  maducoeval2  22661  madugsum  22664  elcls  23096  isclo  23110  ptbasfi  23604  ptopn2  23607  xkopt  23678  kqdisj  23755  fin1aufil  23955  ptcmplem4  24078  opnsubg  24131  tsmssplit  24175  zcld  24848  recld2  24849  reconnlem1  24861  ioombl1lem4  25609  i1fima2sn  25728  itg1val2  25732  i1f0  25735  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1flim  25772  itg2splitlem  25797  itg2split  25798  itg2cnlem1  25810  itg2cnlem2  25811  itgss2  25862  itgeqa  25863  itgss3  25864  itgless  25866  ibladdlem  25869  itgaddlem1  25872  iblabslem  25877  itggt0  25893  itgcn  25894  ply1termlem  26256  plypf1  26265  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeidlem  26290  coeid3  26293  coefv0  26301  coemulc  26308  dvply1  26339  vieta1lem2  26367  aaliou2  26396  logdmnrp  26697  regamcl  27118  lgam1  27121  gam1  27122  facgam  27123  chpub  27278  chebbnd1lem1  27527  numedglnl  29175  strlem1  32278  cycpmco2  33135  2sqr3minply  33752  indval2  33994  ind0  33998  sigaclfu2  34101  eulerpartlemb  34349  mrsubcn  35503  dfon2lem6  35769  lindsadd  37599  ibladdnclem  37662  itgaddnclem1  37664  iblabsnclem  37669  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem8  37686  dvasin  37690  dvacos  37691  pridlc2  38058  pridlc3  38059  idomnnzgmulnz  42114  deg1gprod  42121  readvrec2  42369  readvrec  42370  selvvvval  42571  fsuppssind  42579  irrapx1  42815  pellqrex  42866  qirropth  42895  setindtr  43012  kelac1  43051  flcidc  43158  arearect  43203  areaquad  43204  cantnfub  43310  mpct  45143  difmap  45149  difmapsn  45154  iccdificc  45491  fsumsupp0  45533  mccllem  45552  sumnnodd  45585  fprodcncf  45855  stoweidlem34  45989  stoweidlem44  45999  stirlinglem5  46033  fourierdlem62  46123  fouriersw  46186  elaa2lem  46188  etransclem44  46233  sge0iunmptlemfi  46368  sge0fodjrnlem  46371  meadjiunlem  46420  isomenndlem  46485  hsphoidmvle2  46540  hsphoidmvle  46541  hspdifhsp  46571  hspmbllem2  46582  ovnsubadd2lem  46600  ovolval4lem1  46604  preimagelt  46654  preimalegt  46655