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

Theorem elrab2 3259
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
Hypotheses
Ref Expression
elrab2.1
elrab2.2
Assertion
Ref Expression
elrab2
Distinct variable groups:   ,   ,   ,

Proof of Theorem elrab2
StepHypRef Expression
1 elrab2.2 . . 3
21eleq2i 2535 . 2
3 elrab2.1 . . 3
43elrab 3257 . 2
52, 4bitri 249 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:  elrabsf  3366  pwnss  4617  fvmpti  5955  fvmptss2  5975  tfis  6689  elom  6703  oawordeulem  7222  oeeulem  7269  mapfienlem1  7884  mapfienlem3  7886  mapfien  7887  ordtypelem2  7965  ordtypelem3  7966  ordtypelem9  7972  wemapso2OLD  7998  wemapso2lem  7999  inf3lema  8062  oemapvali  8124  mapfienOLD  8159  tz9.12lem3  8228  cofsmo  8670  enfin2i  8722  fin23lem28  8741  isf32lem6  8759  hsmexlem4  8830  zorn2lem2  8898  pwfseqlem1  9057  pwfseqlem3  9059  nqereu  9328  elz  10891  zsupss  11200  rpnnen1lem5  11241  elrp  11251  repos  11650  wwlktovf  12894  wwlktovf1  12895  wwlktovfo  12896  sqrlem1  13076  sqrlem2  13077  sqrlem6  13081  sqrlem7  13082  ello1  13338  elo1  13349  rlimrege0  13402  divalglem2  14053  divalglem4  14054  divalglem5  14055  divalglem9  14059  divalglem10  14060  bitsfzolem  14084  gcdcllem1  14149  gcdcllem2  14150  gcdcllem3  14151  bezoutlem1  14176  bezoutlem3  14178  bezoutlem4  14179  isprm  14219  maxprmfct  14254  phimullem  14309  eulerthlem1  14311  eulerthlem2  14312  pclem  14362  pcprecl  14363  pcprendvds  14364  infpn2  14431  prmreclem1  14434  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  1arith  14445  elgz  14449  4sqlem13  14475  4sqlem17  14479  4sqlem18  14480  vdwnnlem2  14514  vdwnnlem3  14515  ramtlecl  14518  isdrs  15563  istos  15665  islat  15677  isclat  15739  isdlat  15823  istsr  15847  issgrp  15912  ismnddef  15922  gsumvallem2  16003  isgrp  16061  elnmz  16240  gastacl  16347  gastacos  16348  symgfixelq  16458  psgneldm  16528  sylow1lem2  16619  sylow1lem4  16621  sylow2alem1  16637  sylow2alem2  16638  efgsdm  16748  iscmn  16805  iscyg  16882  iscyggen  16883  dprdw  17043  dprdwOLD  17050  ablfacrplem  17116  ablfacrp  17117  ablfac1c  17122  ablfac1eu  17124  pgpfaclem1  17132  ablfaclem3  17138  ablfac2  17140  issrg  17159  isring  17202  iscrng  17205  isdrng  17400  islmod  17516  islvec  17750  lspsolvlem  17788  lbsextlem1  17804  lbsextlem3  17806  lbsextlem4  17807  islpir  17897  isnzr  17907  isrrg  17936  isdomn  17943  isassa  17964  psrbag  18013  psrbaglefi  18023  psrbaglefiOLD  18024  psrbagconcl  18025  psrbagconf1o  18026  gsumbagdiaglem  18027  mplelbas  18087  mplelbasOLD  18089  isphl  18663  pjdm  18738  ishil  18749  frlmssuvc1  18825  frlmssuvc2  18826  frlmssuvc1OLD  18827  frlmssuvc2OLD  18828  frlmsslsp  18829  frlmsslspOLD  18830  gsummatr01lem1  19157  gsummatr01lem4  19160  gsummatr01  19161  mretopd  19593  neipeltop  19630  isperf  19652  ist0  19821  ist1  19822  ishaus  19823  iscnrm  19824  isreg  19833  isnrm  19836  ispnrm  19840  iscmp  19888  hauscmplem  19906  iscon  19914  concompss  19934  is1stc  19942  islly  19969  isnlly  19970  dfac14lem  20118  ishmeo  20260  ptcmplem3  20554  ptcmplem4  20555  istmd  20573  istgp  20576  tgpconcompeqg  20610  tgpt0  20617  qustgpopn  20618  istrg  20666  istdrg  20668  istlm  20687  istvc  20694  iscusp  20802  imasdsf1olem  20876  isxms  20950  isms  20952  blcld  21008  prdsxmslem2  21032  isngp  21116  isnrg  21169  isnlm  21184  icccmplem1  21327  icccmplem2  21328  isclm  21564  iscph  21617  isbn  21777  iscms  21784  ivthlem1  21863  ivthlem2  21864  ivthlem3  21865  elovolm  21886  ovolicc2lem2  21929  ovolicc2lem4  21931  ovolicc2lem5  21932  ismbl  21937  dyadmbllem  22008  dyadmbl  22009  ismbf1  22033  isi1f  22081  isibl  22172  isuc1p  22541  ismon1p  22543  radcnvle  22815  abelthlem2  22827  abelthlem7a  22832  atans  23261  wilthlem2  23343  wilthlem3  23344  ftalem3  23348  sqff1o  23456  dvdsmulf1o  23470  lgslem2  23572  lgslem3  23573  lgsfcl2  23577  rpvmasumlem  23672  dchrvmaeq0  23689  dchrisum0re  23698  pntlem3  23794  axcontlem2  24268  usgraidx2vlem1  24391  usgraidx2vlem2  24392  cusgraexi  24468  cusgrafilem2  24480  wlknwwlknfun  24710  wlknwwlkninj  24711  wlkiswwlkfun  24717  wlkiswwlkinj  24718  wlkiswwlksur  24719  wwlkextfun  24729  wwlkextinj  24730  wwlkextsur  24731  wwlkextproplem3  24743  clwwlkel  24793  clwwlkf  24794  clwwlkf1  24796  clwlkfclwwlk1hashn  24841  clwlkfoclwwlk  24845  clwlkf1clwwlklem1  24846  clwlkf1clwwlklem2  24847  clwlkf1clwwlklem3  24848  frgrawopreglem3  25046  extwwlkfab  25090  isablo  25285  iscbn  25780  hcau  26101  issh  26125  isch  26140  elcnop  26776  ellnop  26777  elbdop  26779  elhmop  26792  elcnfn  26801  ellnfn  26802  isst  27132  ishst  27133  ela  27258  isomnd  27691  isslmd  27745  isorng  27789  iscref  27847  isrrext  27981  oddpwdc  28293  eulerpartleme  28302  eulerpartlemo  28304  eulerpartlemd  28305  eulerpartlemt0  28308  eulerpartlemf  28309  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemmf  28314  eulerpartlemgvv  28315  eulerpartlemgs2  28319  eulerpartlemn  28320  elprob  28348  ballotlemelo  28426  ballotleme  28435  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgambdd  28579  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem1  28635  ispcon  28668  isscon  28671  cvmsiota  28722  cvmlift2lem12  28759  rdgprc0  29226  elwlim  29379  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  isprrngo  30447  pellqrex  30815  islnm  31023  pwssplit4  31035  islnr  31060  hashgcdlem  31157  stoweidlem14  31796  stoweidlem16  31798  stoweidlem37  31819  stoweidlem48  31830  stoweidlem51  31833  stoweidlem59  31841  usgedgvadf1lem1  32413  usgedgvadf1lem2  32414  usgedgvadf1ALTlem1  32416  usgedgvadf1ALTlem2  32417  0nodd  32498  1odd  32499  2nodd  32500  iscmgmALT  32548  issgrpALT  32549  iscsgrpALT  32550  isrng  32682  1neven  32738  2zlidl  32740  2zrngamgm  32745  2zrngagrp  32749  2zrngmmgm  32752  2zrngnmrid  32756  bnj1152  34054  bnj1280  34076  toycom  34698  isopos  34905  isoml  34963  isatl  35024  iscvlat  35048  ishlat1  35077  cdlemm10N  36845  dihglblem2N  37021  lcfl1lem  37218  lcfls1lem  37261  mapdordlem1a  37361  mapdordlem1  37363
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