Theorem eldifn 4055

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

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

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884

This theorem is referenced by:  elndif  4056  disjel  4364  tz7.7  6185  partfun  6467  funiunfv  6985  tfi  7548  peano5  7585  wfrlem10  7947  wfrlem13  7950  wfrlem16  7953  tz7.48-2  8061  tz7.49  8064  oaf1o  8172  undifixp  8481  domdifsn  8583  isinf  8715  ordtypelem7  8972  unxpwdom2  9036  inf3lem3  9077  infdifsn  9104  cantnfp1lem1  9125  cantnfp1lem3  9127  cantnflem1d  9135  setind  9160  fin23lem30  9753  domtriomlem  9853  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  ttukeylem7  9926  konigthlem  9979  fpwwe2lem13  10053  fpwwe2  10054  hashf1lem1  13809  rlimrecl  14929  sumrblem  15060  fsumcvg  15061  summolem2a  15064  fsumss  15074  sumss2  15075  binomlem  15176  isumltss  15195  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  fprodss  15294  fprodsplit  15312  fprodmodd  15343  sumodd  15729  prmreclem2  16243  prmreclem5  16246  ramub1lem1  16352  efgs1b  18854  gsumzsplit  19040  gsum2d  19085  gsum2d2lem  19086  dmdprdsplitlem  19152  pgpfac1lem1  19189  irredrmul  19453  lbsextlem2  19924  lbsextlem4  19926  cnsubrg  20151  psrlidm  20641  mplcoe1  20705  mplcoe5  20708  evlslem3  20752  maducoeval2  21245  madugsum  21248  elcls  21678  isclo  21692  ptbasfi  22186  ptopn2  22189  xkopt  22260  kqdisj  22337  fin1aufil  22537  ptcmplem4  22660  opnsubg  22713  tsmssplit  22757  zcld  23418  recld2  23419  reconnlem1  23431  ioombl1lem4  24165  i1fima2sn  24284  itg1val2  24288  i1f0  24291  itg1addlem4  24303  mbfi1flim  24327  itg2splitlem  24352  itg2split  24353  itg2cnlem1  24365  itg2cnlem2  24366  itgss2  24416  itgeqa  24417  itgss3  24418  itgless  24420  ibladdlem  24423  itgaddlem1  24426  iblabslem  24431  itggt0  24447  itgcn  24448  ply1termlem  24800  plypf1  24809  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  coeidlem  24834  coeid3  24837  coefv0  24845  coemulc  24852  dvply1  24880  vieta1lem2  24907  aaliou2  24936  logdmnrp  25232  regamcl  25646  lgam1  25649  gam1  25650  facgam  25651  chpub  25804  chebbnd1lem1  26053  numedglnl  26937  strlem1  30033  cycpmco2  30825  indval2  31383  ind0  31387  sigaclfu2  31490  eulerpartlemb  31736  mrsubcn  32879  dfon2lem6  33146  frrlem11  33246  frrlem12  33247  frrlem14  33249  lindsadd  35050  ibladdnclem  35113  itgaddnclem1  35115  iblabsnclem  35120  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem8  35137  dvasin  35141  dvacos  35142  pridlc2  35510  pridlc3  35511  fsuppssind  39459  irrapx1  39769  pellqrex  39820  qirropth  39849  setindtr  39965  kelac1  40007  flcidc  40118  arearect  40165  areaquad  40166  mpct  41830  difmap  41836  difmapsn  41841  iccdificc  42176  fsumsupp0  42220  mccllem  42239  sumnnodd  42272  fprodcncf  42542  stoweidlem34  42676  stoweidlem44  42686  stirlinglem5  42720  fourierdlem62  42810  fouriersw  42873  elaa2lem  42875  etransclem44  42920  sge0iunmptlemfi  43052  sge0fodjrnlem  43055  meadjiunlem  43104  isomenndlem  43169  hsphoidmvle2  43224  hsphoidmvle  43225  hspdifhsp  43255  hspmbllem2  43266  ovnsubadd2lem  43284  ovolval4lem1  43288  preimagelt  43337  preimalegt  43338