MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrab Unicode version

Theorem elrab 3257
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
Hypothesis
Ref Expression
elrab.1
Assertion
Ref Expression
elrab
Distinct variable groups:   ,   ,   ,

Proof of Theorem elrab
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
3 nfv 1707 . 2
4 elrab.1 . 2
51, 2, 3, 4elrabf 3255 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  {crab 2811
This theorem is referenced by:  elrab3  3258  elrab2  3259  ralrab  3261  rexrab  3263  rabsnt  4107  unimax  4285  ssintub  4304  intminss  4313  reusv6OLD  4663  rabxfrd  4673  ssimaex  5938  weniso  6250  canth  6254  sorpsscmpl  6591  onnminsb  6639  dfom2  6702  ssnlim  6718  elsuppfn  6926  ressuppssdif  6940  oeeulem  7269  nnawordex  7305  elpmg  7454  fineqvlem  7754  mapfienlem2  7885  supub  7939  suplub  7940  ordtypelem6  7969  ordtypelem7  7970  hartogslem1  7988  hartogs  7990  wemapsolem  7996  card2on  8001  elharval  8010  wdom2d  8027  cantnfs  8106  oemapvali  8124  cantnfsOLD  8136  rankuni2b  8292  scottex  8324  tskwe  8352  cardid2  8355  iscard2  8378  harval2  8399  cardmin2  8400  acni3  8449  alephsuc2  8482  kmlem1  8551  cofsmo  8670  coftr  8674  fin23lem11  8718  enfin2i  8722  fin1a2lem9  8809  fin1a2lem11  8811  axcc4  8840  axdc3lem2  8852  zorn2lem7  8903  ondomon  8959  alephval2  8968  grutsk  9221  pinq  9326  infm3  10527  infmrcl  10547  nnind  10579  peano2uz2  10975  peano5uzi  10976  dfuzi  10978  uzind  10979  uzind3  10981  uzind3OLD  10983  eluz1  11114  uzind4  11168  nnwos  11178  eqreznegel  11196  zsupss  11200  zmin  11207  elixx1  11567  elioo2  11599  elfz1  11706  flval3  11951  serge0  12161  expge0  12202  expge1  12203  hashbclem  12501  pr2pwpr  12520  elss2pr  12527  wrdmap  12572  disjxwrd  12680  wwlktovfo  12896  shftf  12912  rlimrege0  13402  incexc2  13650  divalglem4  14054  divalgmod  14064  bitsval  14074  bezout  14180  1nprm  14222  1idssfct  14223  isprm2  14225  phicl2  14298  hashdvds  14305  odzval  14318  odzcllem  14319  odzdvds  14322  pcpremul  14367  prmreclem1  14434  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  ramub  14531  rami  14533  ramub1lem1  14544  ramub1lem2  14545  ismre  14987  mrcflem  15003  mrcval  15007  ismri  15028  isacs  15048  isacs1i  15054  catlid  15080  catrid  15081  ismon  15128  isnat  15316  eldmcoa  15392  coaval  15395  lubeldm  15611  glbeldm  15624  gsumress  15903  gsumval2  15907  ismhm  15968  issubm  15978  issubmd  15980  mhmeql  15995  mrcmndind  15997  grplinv  16096  issubg  16201  cycsubg  16229  isnsg  16230  ghmeql  16289  isgim  16310  isga  16329  elcntz  16360  elcntzsn  16363  symgfix2  16441  pmtrval  16476  pmtrrn  16482  symgsssg  16492  symgfisg  16493  psgnunilem5  16519  odid  16562  odlem2  16563  gexid  16601  gexlem2  16602  gexdvds  16604  isslw  16628  pgpssslw  16634  pj1id  16717  efgsfo  16757  oddvdssubg  16861  dprdwd  17044  pgpfac1lem5  17130  ablfaclem2  17137  isirred  17348  isrim0  17372  issubrg  17429  isabv  17468  islss  17581  islmhm  17673  lmhmeql  17701  islmim  17708  islbs  17722  gsumbagdiaglem  18027  psrmulcllem  18040  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  psrass1  18060  psrcom  18064  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  mplmonmul  18126  evlsval2  18189  coe1fsupp  18254  coe1ae0  18257  coe1mul2  18310  zrhcofipsgn  18629  psgndiflemB  18636  elocv  18699  isobs  18751  dsmmelbas  18770  frlmelbas  18788  frlmelbasOLD  18789  frlmssuvc2  18826  frlmssuvc2OLD  18828  islinds  18844  dmatel  18995  dmatmulcl  19002  scmatel  19007  scmateALT  19014  symgmatr01lem  19155  pmatcoe1fsupp  19202  cpmatel  19212  chpscmat  19343  istopon  19426  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  epttop  19510  iscld  19528  clscld  19548  isnei  19604  neips  19614  neiptopnei  19633  iscn  19736  iscnp  19738  ordthauslem  19884  cmpsublem  19899  concompcon  19933  2ndc1stc  19952  2ndcdisj  19957  locfincmp  20027  elkgen  20037  xkoopn  20090  xkoccn  20120  txdis1cn  20136  pthaus  20139  txkgen  20153  xkohaus  20154  xkococnlem  20160  xkococn  20161  xkoinjcn  20188  txcon  20190  elqtop  20198  nrmr0reg  20250  elmptrab  20328  fbssfi  20338  opnfbas  20343  elfg  20372  cfinfil  20394  csdfil  20395  supfil  20396  filssufilg  20412  uffix  20422  fixufil  20423  uffixfr  20424  uffixsn  20426  ufinffr  20430  ufilen  20431  elflim2  20465  supnfcls  20521  fclscf  20526  flimfnfcls  20529  alexsubALTlem2  20548  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem2  20553  tmdgsum2  20595  symgtgp  20600  ghmcnp  20613  elutop  20736  isucn  20781  iscfilu  20791  ispsmet  20808  ismet  20826  isxmet  20827  elblps  20890  elbl  20891  restmetu  21090  icccmp  21330  elcncf  21393  ishtpy  21472  isphtpy  21481  om1elbas  21532  iscfil  21704  iscau  21715  iscmet  21723  lmle  21740  rrxfsupp  21829  minveclem3  21844  minveclem4  21847  ovolshftlem1  21920  ovolscalem1  21924  ovolicc2lem3  21930  iundisj  21958  dyadmax  22007  dyadmbllem  22008  opnmbllem  22010  vitalilem2  22018  vitalilem3  22019  elcpn  22337  ig1pval3  22575  coelem  22623  quotlem  22696  elqaalem1  22715  elqaalem3  22717  aannenlem1  22724  aannenlem2  22725  aalioulem2  22729  radcnv0  22811  dmarea  23287  jensen  23318  ftalem4  23349  ftalem5  23350  efnnfsumcl  23376  efchtdvds  23433  sqff1o  23456  dvdsdivcl  23457  fsumdvdsdiaglem  23459  dvdsppwf1o  23462  dvdsflf1o  23463  dvdsflsumcom  23464  musum  23467  muinv  23469  logfac2  23492  dchrelbas  23511  dchrfi  23530  lgsfle1  23580  lgsle1  23586  lgsdirprm  23604  lgsne0  23608  lgsquadlem1  23629  lgsquadlem2  23630  dchrvmasumlem1  23680  logsqvma  23727  pntleml  23796  tgellng  23940  mircgr  24038  mirbtwn  24039  ttgelitv  24186  umgrale  24321  umgra1  24326  edg  24353  uslgra1  24372  usgra1  24373  usgraedg2  24375  usgraedgrnv  24377  usgrarnedg  24384  usgraedg4  24387  usgraexmpl  24401  usgrares1  24410  nbgrael  24426  nbgraeledg  24430  nbgraf1olem3  24443  cusgrarn  24459  nbcusgra  24463  cusgrares  24472  uvtxel  24489  uvtxnbgra  24493  cusgrauvtxb  24496  iswwlk  24683  iswwlkn  24684  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextsur  24731  wlknwwlknvbij  24740  isclwwlk  24768  isclwwlkn  24769  clwwlkprop  24770  clwwlknprop  24772  clwwlkvbij  24801  clwwlknscsh  24819  eleclclwwlkn  24833  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  el2wlksoton  24878  el2spthsoton  24879  el2wlksotot  24882  rusgranumwlklem0  24948  rusgranumwlklem1  24949  rusgranumwlklem3  24951  rusgranumwlks  24956  eupath2  24980  umgrabi  24983  konigsberg  24987  2spotdisj  25061  usg2spot2nb  25065  usgreg2spot  25067  numclwwlkun  25079  numclwwlkovfel2  25083  numclwwlkovgel  25088  numclwlk1lem2foa  25091  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  grpoidinv2  25220  grpoinv  25229  isssp  25637  islno  25668  isblo  25697  ishmo  25726  ubthlem1  25786  ubthlem2  25787  htthlem  25834  ocel  26199  shsval2i  26305  ococin  26326  chsupsn  26331  eleigvec  26876  cnlnadjlem5  26990  shatomistici  27280  hatomistici  27281  nnindf  27610  ordtconlem1  27906  indf1ofs  28039  sigagenval  28140  ddemeas  28208  ismbfm  28223  imambfm  28233  dya2iocuni  28254  oms0  28266  issibf  28275  sitgfval  28283  oddpwdc  28293  eulerpartlemgh  28317  eulerpartlemgs2  28319  dstfrvel  28412  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemiex  28440  ballotlemfrcn0  28468  ballotlemirc  28470  ballotlem7  28474  conpcon  28680  iscvm  28704  cvmsi  28710  cvmsval  28711  cvmliftmolem2  28727  cvmliftiota  28746  snmlval  28776  elmpst  28896  elgiso  29036  sltval2  29416  sltres  29424  nodenselem7  29447  nofulllem5  29466  lineelsb2  29798  linerflx1  29799  rankeq1o  29828  fin2solem  30039  fin2so  30040  opnmbllem0  30050  mblfinlem2  30052  itg2gt0cn  30070  finminlem  30136  fneint  30166  fnessref  30175  topmeet  30182  topjoin  30183  neifg  30189  indexa  30224  nninfnub  30244  istotbnd  30265  sstotbnd2  30270  isbnd  30276  isrngohom  30368  isrngoiso  30381  isidl  30411  ispridl  30431  ismaxidl  30437  prnc  30464  isfldidl  30465  isnacs  30636  elmzpcl  30658  mzpindd  30678  rencldnfilem  30754  irrapxlem6  30763  pellexlem3  30767  pellexlem5  30769  elpell1qr  30783  elpell14qr  30785  elpell1234qr  30787  pellfundre  30817  pellfundge  30818  pellfundlb  30820  pellfundglb  30821  rmspecnonsq  30843  jm2.22  30937  jm2.23  30938  rpnnen3lem  30973  fnwe2lem2  30997  fnwe2lem3  30998  elmnc  31085  dgraalem  31094  dgraaub  31097  mpaalem  31101  rgspnmin  31120  issdrg  31146  phisum  31159  lcmledvds  31205  lcmgcdlem  31212  nzss  31222  iccshift  31558  iooshift  31562  limcperiod  31634  sumnnodd  31636  ioodvbdlimc1lem1  31728  dvnprodlem1  31743  dvnprodlem3  31745  itgperiod  31780  stoweidlem14  31796  stoweidlem15  31797  stoweidlem16  31798  stoweidlem31  31813  stoweidlem36  31818  stoweidlem46  31828  stoweidlem48  31830  fourierdlem2  31891  fourierdlem3  31892  fourierdlem20  31909  fourierdlem25  31914  fourierdlem37  31926  fourierdlem42  31931  fourierdlem48  31937  fourierdlem51  31940  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem79  31968  fourierdlem81  31970  elaa2lem  32016  etransclem24  32041  etransclem26  32043  etransclem28  32045  etransclem35  32052  etransclem48  32065  ismgmhm  32471  issubmgm  32477  rabsubmgmd  32479  mgmhmeql  32491  assintop  32533  isassintop  32534  assintopcllaw  32536  fncnvimaeqv  32626  isrnghm  32698  isrngisom  32702  0even  32737  2even  32739  2zrngamgm  32745  dmatALTbasel  33003  lcoval  33013  secval  33141  cscval  33142  cotval  33143  islshp  34704  lssats  34737  islfl  34785  isat  35011  atlatmstc  35044  islln  35230  islpln  35254  islvol  35297  linepsubN  35476  elpmap  35482  pmapsub  35492  elpadd  35523  paddvaln0N  35525  islhp  35720  isldil  35834  isltrn  35843  isdilN  35879  istrnN  35882  diaval  36759  diaelval  36760  diaeldm  36763  diaelrnN  36772  cdlemm10N  36845  docaclN  36851  dibglbN  36893  dicval  36903  dicfnN  36910  dicvalrelN  36912  dihglblem2aN  37020  dihglblem2N  37021  dihglblem3N  37022  dih1dimatlem  37056  dihglb2  37069  dochvalr  37084  doch2val2  37091  dochocss  37093  islpolN  37210  mapd0  37392
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-rab 2816  df-v 3111
  Copyright terms: Public domain W3C validator