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

Theorem elrab2 3245
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
Hypotheses
Ref Expression
elrab2.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
elrab2.2  |-  C  =  { x  e.  B  |  ph }
Assertion
Ref Expression
elrab2  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem elrab2
StepHypRef Expression
1 elrab2.2 . . 3  |-  C  =  { x  e.  B  |  ph }
21eleq2i 2521 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3243 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 249 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    e. wcel 1804   {crab 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097
This theorem is referenced by:  elrabsf  3352  pwnss  4602  fvmpti  5940  fvmptss2  5960  tfis  6674  elom  6688  oawordeulem  7205  oeeulem  7252  mapfienlem1  7866  mapfienlem3  7868  mapfien  7869  ordtypelem2  7947  ordtypelem3  7948  ordtypelem9  7954  wemapso2OLD  7980  wemapso2lem  7981  inf3lema  8044  oemapvali  8106  mapfienOLD  8141  tz9.12lem3  8210  cofsmo  8652  enfin2i  8704  fin23lem28  8723  isf32lem6  8741  hsmexlem4  8812  zorn2lem2  8880  pwfseqlem1  9039  pwfseqlem3  9041  nqereu  9310  elz  10873  zsupss  11181  rpnnen1lem5  11222  elrp  11232  repos  11631  wwlktovf  12875  wwlktovf1  12876  wwlktovfo  12877  sqrlem1  13057  sqrlem2  13058  sqrlem6  13062  sqrlem7  13063  ello1  13319  elo1  13330  rlimrege0  13383  divalglem2  14034  divalglem4  14035  divalglem5  14036  divalglem9  14040  divalglem10  14041  bitsfzolem  14065  gcdcllem1  14130  gcdcllem2  14131  gcdcllem3  14132  bezoutlem1  14157  bezoutlem3  14159  bezoutlem4  14160  isprm  14200  maxprmfct  14235  phimullem  14290  eulerthlem1  14292  eulerthlem2  14293  pclem  14343  pcprecl  14344  pcprendvds  14345  infpn2  14412  prmreclem1  14415  prmreclem2  14416  prmreclem3  14417  prmreclem5  14419  1arith  14426  elgz  14430  4sqlem13  14456  4sqlem17  14460  4sqlem18  14461  vdwnnlem2  14495  vdwnnlem3  14496  ramtlecl  14499  isdrs  15541  istos  15643  islat  15655  isclat  15717  isdlat  15801  istsr  15825  issgrp  15890  ismnddef  15900  gsumvallem2  15981  isgrp  16039  elnmz  16218  gastacl  16325  gastacos  16326  symgfixelq  16436  psgneldm  16506  sylow1lem2  16597  sylow1lem4  16599  sylow2alem1  16615  sylow2alem2  16616  efgsdm  16726  iscmn  16783  iscyg  16860  iscyggen  16861  dprdw  17021  dprdwOLD  17028  ablfacrplem  17094  ablfacrp  17095  ablfac1c  17100  ablfac1eu  17102  pgpfaclem1  17110  ablfaclem3  17116  ablfac2  17118  issrg  17137  isring  17180  iscrng  17183  isdrng  17378  islmod  17494  islvec  17728  lspsolvlem  17766  lbsextlem1  17782  lbsextlem3  17784  lbsextlem4  17785  islpir  17875  isnzr  17885  isrrg  17914  isdomn  17921  isassa  17942  psrbag  17991  psrbaglefi  18001  psrbaglefiOLD  18002  psrbagconcl  18003  psrbagconf1o  18004  gsumbagdiaglem  18005  mplelbas  18065  mplelbasOLD  18067  isphl  18640  pjdm  18715  ishil  18726  frlmssuvc1  18802  frlmssuvc2  18803  frlmssuvc1OLD  18804  frlmssuvc2OLD  18805  frlmsslsp  18806  frlmsslspOLD  18807  gsummatr01lem1  19134  gsummatr01lem4  19137  gsummatr01  19138  mretopd  19570  neipeltop  19607  isperf  19629  ist0  19798  ist1  19799  ishaus  19800  iscnrm  19801  isreg  19810  isnrm  19813  ispnrm  19817  iscmp  19865  hauscmplem  19883  iscon  19891  concompss  19911  is1stc  19919  islly  19946  isnlly  19947  dfac14lem  20095  ishmeo  20237  ptcmplem3  20531  ptcmplem4  20532  istmd  20550  istgp  20553  tgpconcompeqg  20587  tgpt0  20594  qustgpopn  20595  istrg  20643  istdrg  20645  istlm  20664  istvc  20671  iscusp  20779  imasdsf1olem  20853  isxms  20927  isms  20929  blcld  20985  prdsxmslem2  21009  isngp  21093  isnrg  21146  isnlm  21161  icccmplem1  21304  icccmplem2  21305  isclm  21541  iscph  21594  isbn  21754  iscms  21761  ivthlem1  21840  ivthlem2  21841  ivthlem3  21842  elovolm  21863  ovolicc2lem2  21906  ovolicc2lem4  21908  ovolicc2lem5  21909  ismbl  21914  dyadmbllem  21985  dyadmbl  21986  ismbf1  22010  isi1f  22058  isibl  22149  isuc1p  22518  ismon1p  22520  radcnvle  22791  abelthlem2  22803  abelthlem7a  22808  atans  23237  wilthlem2  23319  wilthlem3  23320  ftalem3  23324  sqff1o  23432  dvdsmulf1o  23446  lgslem2  23548  lgslem3  23549  lgsfcl2  23553  rpvmasumlem  23648  dchrvmaeq0  23665  dchrisum0re  23674  pntlem3  23770  axcontlem2  24244  usgraidx2vlem1  24367  usgraidx2vlem2  24368  cusgraexi  24444  cusgrafilem2  24456  wlknwwlknfun  24686  wlknwwlkninj  24687  wlkiswwlkfun  24693  wlkiswwlkinj  24694  wlkiswwlksur  24695  wwlkextfun  24705  wwlkextinj  24706  wwlkextsur  24707  wwlkextproplem3  24719  clwwlkel  24769  clwwlkf  24770  clwwlkf1  24772  clwlkfclwwlk1hashn  24817  clwlkfoclwwlk  24821  clwlkf1clwwlklem1  24822  clwlkf1clwwlklem2  24823  clwlkf1clwwlklem3  24824  frgrawopreglem3  25022  extwwlkfab  25066  isablo  25261  iscbn  25756  hcau  26077  issh  26101  isch  26116  elcnop  26752  ellnop  26753  elbdop  26755  elhmop  26768  elcnfn  26777  ellnfn  26778  isst  27108  ishst  27109  ela  27234  isomnd  27668  isslmd  27722  isorng  27766  iscref  27824  isrrext  27958  oddpwdc  28270  eulerpartleme  28279  eulerpartlemo  28281  eulerpartlemd  28282  eulerpartlemt0  28285  eulerpartlemf  28286  eulerpartlemt  28287  eulerpartlemr  28290  eulerpartlemmf  28291  eulerpartlemgvv  28292  eulerpartlemgs2  28296  eulerpartlemn  28297  elprob  28325  ballotlemelo  28403  ballotleme  28412  lgamgulmlem2  28549  lgamgulmlem3  28550  lgamgulmlem5  28552  lgambdd  28556  subfacp1lem3  28603  subfacp1lem5  28605  erdszelem1  28612  ispcon  28645  isscon  28648  cvmsiota  28699  cvmlift2lem12  28736  rdgprc0  29201  elwlim  29354  neibastop1  30152  neibastop2lem  30153  neibastop2  30154  isprrngo  30422  pellqrex  30790  islnm  30998  pwssplit4  31010  islnr  31035  hashgcdlem  31133  stoweidlem14  31685  stoweidlem16  31687  stoweidlem37  31708  stoweidlem48  31719  stoweidlem51  31722  stoweidlem59  31730  usgedgvadf1lem1  32251  usgedgvadf1lem2  32252  usgedgvadf1ALTlem1  32254  usgedgvadf1ALTlem2  32255  0nodd  32335  1odd  32336  2nodd  32337  iscmgmALT  32385  issgrpALT  32386  iscsgrpALT  32387  isrng  32403  1neven  32448  2zlidl  32450  2zrngamgm  32455  2zrngagrp  32459  2zrngmmgm  32462  2zrngnmrid  32466  bnj1152  33787  bnj1280  33809  toycom  34438  isopos  34645  isoml  34703  isatl  34764  iscvlat  34788  ishlat1  34817  cdlemm10N  36585  dihglblem2N  36761  lcfl1lem  36958  lcfls1lem  37001  mapdordlem1a  37101  mapdordlem1  37103
  Copyright terms: Public domain W3C validator