Theorem eldifn 4094

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916

This theorem is referenced by:  elndif  4095  disjel  4423  tz7.7  6389  partfun  6685  funiunfv  7249  tfi  7851  peano5  7892  resf1extb  7933  frrlem11  8295  frrlem12  8296  frrlem14  8298  tz7.48-2  8431  tz7.49  8434  oaf1o  8550  undifixp  8934  domdifsn  9050  isinf  9227  ordtypelem7  9488  unxpwdom2  9552  inf3lem3  9601  infdifsn  9628  cantnfp1lem1  9649  cantnfp1lem3  9651  cantnflem1d  9659  setind  9718  fin23lem30  10328  domtriomlem  10428  axdc3lem4  10439  axdc4lem  10441  axcclem  10443  ttukeylem7  10501  konigthlem  10555  fpwwe2lem12  10629  fpwwe2  10630  indval2  12225  ind0  12230  hashf1lem1  14494  rlimrecl  15633  sumrblem  15764  fsumcvg  15765  summolem2a  15768  fsumss  15778  sumss2  15779  binomlem  15885  isumltss  15904  prodrblem  15985  fprodcvg  15986  prodmolem2a  15990  fprodss  16004  fprodsplit  16022  fprodmodd  16053  sumodd  16448  prmreclem2  16979  prmreclem5  16982  ramub1lem1  17088  chnccat  18684  efgs1b  19808  gsumzsplit  19999  gsum2d  20044  gsum2d2lem  20045  dmdprdsplitlem  20111  pgpfac1lem1  20148  irredrmul  20511  lbsextlem2  21263  lbsextlem4  21265  cnsubrg  21548  psrlidm  22082  mplcoe1  22159  mplcoe5  22162  evlslem3  22202  selvvvval  22264  maducoeval2  22768  madugsum  22771  elcls  23201  isclo  23215  ptbasfi  23709  ptopn2  23712  xkopt  23783  kqdisj  23860  fin1aufil  24060  ptcmplem4  24183  opnsubg  24236  tsmssplit  24280  zcld  24942  recld2  24943  reconnlem1  24955  ioombl1lem4  25691  i1fima2sn  25810  itg1val2  25814  i1f0  25817  itg1addlem4  25829  mbfi1flim  25853  itg2splitlem  25878  itg2split  25879  itg2cnlem1  25891  itg2cnlem2  25892  itgss2  25943  itgeqa  25944  itgss3  25945  itgless  25947  ibladdlem  25950  itgaddlem1  25953  iblabslem  25958  itggt0  25974  itgcn  25975  ply1termlem  26331  plypf1  26340  plyaddlem1  26341  plymullem1  26342  coeeulem  26352  coeidlem  26365  coeid3  26368  coefv0  26376  coemulc  26383  dvply1  26416  vieta1lem2  26443  aaliou2  26472  logdmnrp  26774  regamcl  27193  lgam1  27196  gam1  27197  facgam  27198  chpub  27352  chebbnd1lem1  27601  numedglnl  29437  strlem1  32545  cycpmco2  33396  2sqr3minply  34117  sigaclfu2  34458  eulerpartlemb  34705  fineqvnttrclse  35472  setindregs  35478  mrsubcn  35946  dfon2lem6  36213  lindsadd  38189  ibladdnclem  38252  itgaddnclem1  38254  iblabsnclem  38259  ftc1anclem5  38273  ftc1anclem6  38274  ftc1anclem8  38276  dvasin  38280  dvacos  38281  pridlc2  38648  pridlc3  38649  idomnnzgmulnz  42827  deg1gprod  42834  readvrec2  43049  readvrec  43050  fsuppssind  43254  irrapx1  43484  pellqrex  43535  qirropth  43564  setindtr  43680  kelac1  43719  flcidc  43826  arearect  43871  areaquad  43872  cantnfub  43977  mpct  45847  difmap  45852  difmapsn  45857  iccdificc  46184  fsumsupp0  46223  mccllem  46242  sumnnodd  46275  fprodcncf  46543  stoweidlem34  46677  stoweidlem44  46687  stirlinglem5  46721  fourierdlem62  46811  fouriersw  46874  elaa2lem  46876  etransclem44  46921  sge0iunmptlemfi  47056  sge0fodjrnlem  47059  meadjiunlem  47108  isomenndlem  47173  hsphoidmvle2  47228  hsphoidmvle  47229  hspdifhsp  47259  hspmbllem2  47270  ovnsubadd2lem  47288  ovolval4lem1  47292  preimagelt  47342  preimalegt  47343  tannpoly  47553