Theorem eldifn 4127

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

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

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 3951

This theorem is referenced by:  elndif  4128  disjel  4456  tz7.7  6388  partfun  6695  funiunfv  7244  tfi  7839  peano5  7881  peano5OLD  7882  frrlem11  8278  frrlem12  8279  frrlem14  8281  wfrlem10OLD  8315  wfrlem13OLD  8318  wfrlem16OLD  8321  tz7.48-2  8439  tz7.49  8442  oaf1o  8560  undifixp  8925  domdifsn  9051  isinf  9257  isinfOLD  9258  ordtypelem7  9516  unxpwdom2  9580  inf3lem3  9622  infdifsn  9649  cantnfp1lem1  9670  cantnfp1lem3  9672  cantnflem1d  9680  setind  9726  fin23lem30  10334  domtriomlem  10434  axdc3lem4  10445  axdc4lem  10447  axcclem  10449  ttukeylem7  10507  konigthlem  10560  fpwwe2lem12  10634  fpwwe2  10635  hashf1lem1  14412  hashf1lem1OLD  14413  rlimrecl  15521  sumrblem  15654  fsumcvg  15655  summolem2a  15658  fsumss  15668  sumss2  15669  binomlem  15772  isumltss  15791  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  fprodss  15889  fprodsplit  15907  fprodmodd  15938  sumodd  16328  prmreclem2  16847  prmreclem5  16850  ramub1lem1  16956  efgs1b  19599  gsumzsplit  19790  gsum2d  19835  gsum2d2lem  19836  dmdprdsplitlem  19902  pgpfac1lem1  19939  irredrmul  20234  lbsextlem2  20765  lbsextlem4  20767  cnsubrg  20998  psrlidm  21515  mplcoe1  21584  mplcoe5  21587  evlslem3  21635  maducoeval2  22134  madugsum  22137  elcls  22569  isclo  22583  ptbasfi  23077  ptopn2  23080  xkopt  23151  kqdisj  23228  fin1aufil  23428  ptcmplem4  23551  opnsubg  23604  tsmssplit  23648  zcld  24321  recld2  24322  reconnlem1  24334  ioombl1lem4  25070  i1fima2sn  25189  itg1val2  25193  i1f0  25196  itg1addlem4  25208  itg1addlem4OLD  25209  mbfi1flim  25233  itg2splitlem  25258  itg2split  25259  itg2cnlem1  25271  itg2cnlem2  25272  itgss2  25322  itgeqa  25323  itgss3  25324  itgless  25326  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  itggt0  25353  itgcn  25354  ply1termlem  25709  plypf1  25718  plyaddlem1  25719  plymullem1  25720  coeeulem  25730  coeidlem  25743  coeid3  25746  coefv0  25754  coemulc  25761  dvply1  25789  vieta1lem2  25816  aaliou2  25845  logdmnrp  26141  regamcl  26555  lgam1  26558  gam1  26559  facgam  26560  chpub  26713  chebbnd1lem1  26962  numedglnl  28394  strlem1  31491  cycpmco2  32280  indval2  33001  ind0  33005  sigaclfu2  33108  eulerpartlemb  33356  mrsubcn  34499  dfon2lem6  34749  lindsadd  36470  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem8  36557  dvasin  36561  dvacos  36562  pridlc2  36929  pridlc3  36930  selvvvval  41155  fsuppssind  41163  irrapx1  41552  pellqrex  41603  qirropth  41632  setindtr  41749  kelac1  41791  flcidc  41902  arearect  41950  areaquad  41951  cantnfub  42057  mpct  43886  difmap  43892  difmapsn  43897  iccdificc  44239  fsumsupp0  44281  mccllem  44300  sumnnodd  44333  fprodcncf  44603  stoweidlem34  44737  stoweidlem44  44747  stirlinglem5  44781  fourierdlem62  44871  fouriersw  44934  elaa2lem  44936  etransclem44  44981  sge0iunmptlemfi  45116  sge0fodjrnlem  45119  meadjiunlem  45168  isomenndlem  45233  hsphoidmvle2  45288  hsphoidmvle  45289  hspdifhsp  45319  hspmbllem2  45330  ovnsubadd2lem  45348  ovolval4lem1  45352  preimagelt  45402  preimalegt  45403