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

Theorem elrab2 3186
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 2541 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3184 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 257 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   {crab 2760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033
This theorem is referenced by:  elrabsf  3294  pwnss  4566  fvmpti  5962  fvmptss2  5984  tfis  6700  elom  6714  oawordeulem  7273  oeeulem  7320  mapfienlem1  7936  mapfienlem3  7938  mapfien  7939  ordtypelem2  8052  ordtypelem3  8053  ordtypelem9  8059  wemapso2lem  8085  inf3lema  8147  oemapvali  8207  tz9.12lem3  8278  cofsmo  8717  enfin2i  8769  fin23lem28  8788  isf32lem6  8806  hsmexlem4  8877  zorn2lem2  8945  pwfseqlem1  9101  pwfseqlem3  9103  nqereu  9372  elz  10963  zsupss  11276  rpnnen1lem5  11317  elrp  11327  repos  11756  wwlktovf  13106  wwlktovf1  13107  wwlktovfo  13108  sqrlem1  13383  sqrlem2  13384  sqrlem6  13388  sqrlem7  13389  ello1  13656  elo1  13667  rlimrege0  13720  divalglem2  14452  divalglem2OLD  14453  divalglem4  14454  divalglem5OLD  14455  divalglem5  14456  divalglem9  14460  divalglem9OLD  14461  divalglem10  14462  bitsfzolem  14486  bitsfzolemOLD  14487  gcdcllem1  14552  gcdcllem2  14553  gcdcllem3  14554  bezoutlem1  14582  bezoutlem3OLD  14584  bezoutlem4OLD  14585  bezoutlem3  14587  bezoutlem4  14588  isprm  14703  maxprmfct  14731  phimullem  14806  eulerthlem1  14808  eulerthlem2  14809  pclem  14867  pcprecl  14868  pcprendvds  14869  infpn2  14936  prmreclem1  14939  prmreclem2  14940  prmreclem3  14941  prmreclem5  14943  1arith  14950  elgz  14954  4sqlem13OLD  14980  4sqlem17OLD  14984  4sqlem18OLD  14985  4sqlem13  14986  4sqlem17  14990  4sqlem18  14991  vdwnnlem2  15025  vdwnnlem3  15026  ramtlecl  15030  isdrs  16257  istos  16359  islat  16371  isclat  16433  isdlat  16517  istsr  16541  issgrp  16606  ismnddef  16616  gsumvallem2  16697  isgrp  16755  elnmz  16934  gastacl  17041  gastacos  17042  symgfixelq  17152  psgneldm  17222  sylow1lem2  17329  sylow1lem4  17331  sylow2alem1  17347  sylow2alem2  17348  efgsdm  17458  iscmn  17515  iscyg  17592  iscyggen  17593  dprdw  17720  ablfacrplem  17776  ablfacrp  17777  ablfac1c  17782  ablfac1eu  17784  pgpfaclem1  17792  ablfaclem3  17798  ablfac2  17800  issrg  17819  isring  17862  iscrng  17865  isdrng  18057  islmod  18173  islvec  18405  lspsolvlem  18443  lbsextlem1  18459  lbsextlem3  18461  lbsextlem4  18462  islpir  18550  isnzr  18560  isrrg  18589  isdomn  18595  isassa  18616  psrbag  18665  psrbaglefi  18673  psrbagconcl  18674  psrbagconf1o  18675  gsumbagdiaglem  18676  mplelbas  18731  isphl  19272  pjdm  19347  ishil  19358  frlmssuvc1  19429  frlmssuvc2  19430  frlmsslsp  19431  gsummatr01lem1  19757  gsummatr01lem4  19760  gsummatr01  19761  mretopd  20185  neipeltop  20222  isperf  20244  ist0  20413  ist1  20414  ishaus  20415  iscnrm  20416  isreg  20425  isnrm  20428  ispnrm  20432  iscmp  20480  hauscmplem  20498  iscon  20505  concompss  20525  is1stc  20533  islly  20560  isnlly  20561  dfac14lem  20709  ishmeo  20851  ptcmplem3  21147  ptcmplem4  21148  istmd  21167  istgp  21170  tgpconcompeqg  21204  tgpt0  21211  qustgpopn  21212  istrg  21256  istdrg  21258  istlm  21277  istvc  21284  iscusp  21392  imasdsf1olem  21466  isxms  21540  isms  21542  blcld  21598  prdsxmslem2  21622  isngp  21688  isnrg  21741  isnlm  21756  icccmplem1  21918  icccmplem2  21919  isclm  22173  iscph  22226  isbn  22384  iscms  22391  ivthlem1  22480  ivthlem2  22481  ivthlem3  22482  elovolm  22506  ovolicc2lem2  22549  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2lem5  22553  ismbl  22558  dyadmbllem  22636  dyadmbl  22637  ismbf1  22661  isi1f  22711  isibl  22802  isuc1p  23170  ismon1p  23172  radcnvle  23454  abelthlem2  23466  abelthlem7a  23471  atans  23935  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamgulmlem5  24037  lgambdd  24041  wilthlem2  24073  wilthlem3  24074  ftalem3  24078  sqff1o  24188  dvdsmulf1o  24202  lgslem2  24304  lgslem3  24305  lgsfcl2  24309  rpvmasumlem  24404  dchrvmaeq0  24421  dchrisum0re  24430  pntlem3  24526  axcontlem2  25074  usgraidx2vlem1  25197  usgraidx2vlem2  25198  cusgraexi  25275  cusgrafilem2  25287  wlknwwlknfun  25517  wlknwwlkninj  25518  wlkiswwlkfun  25524  wlkiswwlkinj  25525  wlkiswwlksur  25526  wwlkextfun  25536  wwlkextinj  25537  wwlkextsur  25538  wwlkextproplem3  25550  clwwlkel  25600  clwwlkf  25601  clwwlkf1  25603  clwlkfclwwlk1hashn  25648  clwlkfoclwwlk  25652  clwlkf1clwwlklem1  25653  clwlkf1clwwlklem2  25654  clwlkf1clwwlklem3  25655  frgrawopreglem3  25853  extwwlkfab  25897  isablo  26092  iscbn  26587  hcau  26918  issh  26942  isch  26956  elcnop  27591  ellnop  27592  elbdop  27594  elhmop  27607  elcnfn  27616  ellnfn  27617  isst  27947  ishst  27948  ela  28073  isomnd  28538  isslmd  28592  isorng  28636  iscref  28745  isrrext  28878  ispisys  29048  isldsys  29052  isros  29064  issros  29071  oddpwdc  29260  eulerpartleme  29269  eulerpartlemo  29271  eulerpartlemd  29272  eulerpartlemt0  29275  eulerpartlemf  29276  eulerpartlemt  29277  eulerpartlemr  29280  eulerpartlemmf  29281  eulerpartlemgvv  29282  eulerpartlemgs2  29286  eulerpartlemn  29287  elprob  29315  ballotlemelo  29393  ballotleme  29402  bnj1152  29879  bnj1280  29901  subfacp1lem3  29977  subfacp1lem5  29979  erdszelem1  29986  ispcon  30018  isscon  30021  cvmsiota  30072  cvmlift2lem12  30109  rdgprc0  30511  elwlim  30577  neibastop1  31086  neibastop2lem  31087  neibastop2  31088  topdifinffinlem  31820  poimirlem5  32009  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  isprrngo  32347  toycom  32610  isopos  32817  isoml  32875  isatl  32936  iscvlat  32960  ishlat1  32989  cdlemm10N  34757  dihglblem2N  34933  lcfl1lem  35130  lcfls1lem  35173  mapdordlem1a  35273  mapdordlem1  35275  pellqrex  35797  islnm  36006  pwssplit4  36018  islnr  36041  hashgcdlem  36145  stoweidlem14  37986  stoweidlem16  37988  stoweidlem37  38010  stoweidlem48  38021  stoweidlem51  38024  stoweidlem59  38032  salexct  38305  salexct2  38310  salexct3  38313  salgencntex  38314  salgensscntex  38315  ovn0lem  38505  opnvonmbllem1  38572  ovolval5lem2  38593  m1expevenALTV  38922  iseven2  38926  isodd3  38927  odd2np1ALTV  38948  opoeALTV  38957  opeoALTV  38958  isgbe  38997  isgbo  38998  isgboa  38999  lfgredgge2  39369  uspgredg2vlem  39464  uspgredg2v  39465  usgredg2vlem1  39466  usgredg2vlem2  39467  ushgredgedga  39470  ushgredgedgaloop  39472  uhgrspan1  39539  isfusgr  39549  nbupgrres  39602  iscusgr  39650  cusgrexi  39672  cusgrfilem2  39682  usgedgvadf1lem1  40233  usgedgvadf1lem2  40234  usgedgvadf1ALTlem1  40236  usgedgvadf1ALTlem2  40237  0nodd  40318  1odd  40319  2nodd  40320  iscmgmALT  40368  issgrpALT  40369  iscsgrpALT  40370  isrng  40384  1neven  40440  2zlidl  40442  2zrngamgm  40447  2zrngagrp  40451  2zrngmmgm  40454  2zrngnmrid  40458
  Copyright terms: Public domain W3C validator