Theorem eldifn 3626

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 3485	. 2
2	1	simprbi 464	1

Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  \cdif 3472

This theorem is referenced by:  elndif  3627  noel  3788  disjel  3873  tz7.7  4909  funiunfv  6160  tfi  6688  peano5  6723  tz7.48-2  7126  tz7.49  7129  oaf1o  7231  undifixp  7525  domdifsn  7620  isinf  7753  ordtypelem7  7970  unxpwdom2  8035  inf3lem3  8068  infdifsn  8094  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnflem1d  8128  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  setind  8186  fin23lem30  8743  domtriomlem  8843  axdc3lem4  8854  axdc4lem  8856  axcclem  8858  ttukeylem7  8916  konigthlem  8964  fpwwe2lem13  9041  fpwwe2  9042  hashf1lem1  12504  rlimrecl  13403  sumrblem  13533  fsumcvg  13534  summolem2a  13537  fsumss  13547  sumss2  13548  binomlem  13641  isumltss  13660  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  fprodss  13755  fprodsplit  13770  prmreclem2  14435  prmreclem5  14438  ramub1lem1  14544  efgs1b  16754  gsumzsplit  16944  gsumzsplitOLD  16945  gsum2d  16999  gsum2dOLD  17000  gsum2d2lem  17001  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  pgpfac1lem1  17125  irredrmul  17356  lbsextlem2  17805  lbsextlem4  17807  psrlidm  18056  psrlidmOLD  18057  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlslem3  18183  evlslem1  18184  cnsubrg  18478  maducoeval2  19142  madugsum  19145  elcls  19574  isclo  19588  ptbasfi  20082  ptopn2  20085  xkopt  20156  kqdisj  20233  fin1aufil  20433  ptcmplem4  20555  opnsubg  20606  tsmssplit  20654  zcld  21318  recld2  21319  reconnlem1  21331  ioombl1lem4  21971  i1fima2sn  22087  itg1val2  22091  i1f0  22094  itg1addlem4  22106  mbfi1flim  22130  itg2splitlem  22155  itg2split  22156  itg2cnlem1  22168  itg2cnlem2  22169  itgss2  22219  itgeqa  22220  itgss3  22221  itgless  22223  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  itggt0  22248  itgcn  22249  ply1termlem  22600  plypf1  22609  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  coeidlem  22634  coeid3  22637  coefv0  22645  coemulc  22652  dvply1  22680  vieta1lem2  22707  aaliou2  22736  logdmnrp  23022  chpub  23495  chebbnd1lem1  23654  strlem1  27169  partfun  27516  elzdif0  27961  indval2  28028  ind0  28033  sigaclfu2  28121  eulerpartlemb  28307  regamcl  28603  lgam1  28606  gam1  28607  facgam  28608  mrsubcn  28879  dfon2lem6  29220  wfrlem10  29352  wfrlem13  29355  wfrlem16  29358  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem8  30097  dvasin  30103  dvacos  30104  pridlc2  30469  pridlc3  30470  irrapx1  30764  pellqrex  30815  qirropth  30844  setindtr  30966  kelac1  31009  flcidc  31123  arearect  31183  areaquad  31184  mccllem  31605  sumnnodd  31636  fprodcncf  31704  stoweidlem34  31816  stoweidlem44  31826  stirlinglem5  31860  fourierdlem62  31951  fouriersw  32014  elaa2lem  32016  etransclem44  32061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478