Theorem eldifn 4103

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110   ∖ cdif 3932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938

This theorem is referenced by:  elndif  4104  noelOLD  4296  disjel  4405  tz7.7  6216  funiunfv  7006  tfi  7567  peano5  7604  wfrlem10  7963  wfrlem13  7966  wfrlem16  7969  tz7.48-2  8077  tz7.49  8080  oaf1o  8188  undifixp  8497  domdifsn  8599  isinf  8730  ordtypelem7  8987  unxpwdom2  9051  inf3lem3  9092  infdifsn  9119  cantnfp1lem1  9140  cantnfp1lem3  9142  cantnflem1d  9150  setind  9175  fin23lem30  9763  domtriomlem  9863  axdc3lem4  9874  axdc4lem  9876  axcclem  9878  ttukeylem7  9936  konigthlem  9989  fpwwe2lem13  10063  fpwwe2  10064  hashf1lem1  13812  rlimrecl  14936  sumrblem  15067  fsumcvg  15068  summolem2a  15071  fsumss  15081  sumss2  15082  binomlem  15183  isumltss  15202  prodrblem  15282  fprodcvg  15283  prodmolem2a  15287  fprodss  15301  fprodsplit  15319  fprodmodd  15350  sumodd  15738  prmreclem2  16252  prmreclem5  16255  ramub1lem1  16361  efgs1b  18861  gsumzsplit  19046  gsum2d  19091  gsum2d2lem  19092  dmdprdsplitlem  19158  pgpfac1lem1  19195  irredrmul  19456  lbsextlem2  19930  lbsextlem4  19932  psrlidm  20182  mplcoe1  20245  mplcoe5  20248  evlslem3  20292  cnsubrg  20604  maducoeval2  21248  madugsum  21251  elcls  21680  isclo  21694  ptbasfi  22188  ptopn2  22191  xkopt  22262  kqdisj  22339  fin1aufil  22539  ptcmplem4  22662  opnsubg  22715  tsmssplit  22759  zcld  23420  recld2  23421  reconnlem1  23433  ioombl1lem4  24161  i1fima2sn  24280  itg1val2  24284  i1f0  24287  itg1addlem4  24299  mbfi1flim  24323  itg2splitlem  24348  itg2split  24349  itg2cnlem1  24361  itg2cnlem2  24362  itgss2  24412  itgeqa  24413  itgss3  24414  itgless  24416  ibladdlem  24419  itgaddlem1  24422  iblabslem  24427  itggt0  24441  itgcn  24442  ply1termlem  24792  plypf1  24801  plyaddlem1  24802  plymullem1  24803  coeeulem  24813  coeidlem  24826  coeid3  24829  coefv0  24837  coemulc  24844  dvply1  24872  vieta1lem2  24899  aaliou2  24928  logdmnrp  25223  regamcl  25637  lgam1  25640  gam1  25641  facgam  25642  chpub  25795  chebbnd1lem1  26044  numedglnl  26928  strlem1  30026  partfun  30420  cycpmco2  30775  indval2  31273  ind0  31277  sigaclfu2  31380  eulerpartlemb  31626  mrsubcn  32766  dfon2lem6  33033  frrlem11  33133  frrlem12  33134  frrlem14  33136  lindsadd  34884  ibladdnclem  34947  itgaddnclem1  34949  iblabsnclem  34954  ftc1anclem5  34970  ftc1anclem6  34971  ftc1anclem8  34973  dvasin  34977  dvacos  34978  pridlc2  35349  pridlc3  35350  irrapx1  39423  pellqrex  39474  qirropth  39503  setindtr  39619  kelac1  39661  flcidc  39772  arearect  39820  areaquad  39821  mpct  41462  difmap  41468  difmapsn  41473  iccdificc  41813  fsumsupp0  41857  mccllem  41876  sumnnodd  41909  fprodcncf  42182  stoweidlem34  42318  stoweidlem44  42328  stirlinglem5  42362  fourierdlem62  42452  fouriersw  42515  elaa2lem  42517  etransclem44  42562  sge0iunmptlemfi  42694  sge0fodjrnlem  42697  iundjiunlem  42740  meadjiunlem  42746  isomenndlem  42811  hsphoidmvle2  42866  hsphoidmvle  42867  hspdifhsp  42897  hspmbllem2  42908  ovnsubadd2lem  42926  ovolval4lem1  42930  preimagelt  42979  preimalegt  42980