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

Theorem elrab2 3237
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 2507 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3235 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 252 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870   {crab 2786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089
This theorem is referenced by:  elrabsf  3344  pwnss  4590  fvmpti  5963  fvmptss2  5985  tfis  6695  elom  6709  oawordeulem  7263  oeeulem  7310  mapfienlem1  7924  mapfienlem3  7926  mapfien  7927  ordtypelem2  8034  ordtypelem3  8035  ordtypelem9  8041  wemapso2lem  8067  inf3lema  8129  oemapvali  8188  tz9.12lem3  8259  cofsmo  8697  enfin2i  8749  fin23lem28  8768  isf32lem6  8786  hsmexlem4  8857  zorn2lem2  8925  pwfseqlem1  9082  pwfseqlem3  9084  nqereu  9353  elz  10939  zsupss  11253  rpnnen1lem5  11294  elrp  11304  repos  11731  wwlktovf  13010  wwlktovf1  13011  wwlktovfo  13012  sqrlem1  13285  sqrlem2  13286  sqrlem6  13290  sqrlem7  13291  ello1  13557  elo1  13568  rlimrege0  13621  divalglem2  14351  divalglem4  14352  divalglem5  14353  divalglem9  14357  divalglem10  14358  bitsfzolem  14382  gcdcllem1  14447  gcdcllem2  14448  gcdcllem3  14449  bezoutlem1  14477  bezoutlem3  14479  bezoutlem4  14480  isprm  14586  maxprmfct  14614  phimullem  14687  eulerthlem1  14689  eulerthlem2  14690  pclem  14742  pcprecl  14743  pcprendvds  14744  infpn2  14811  prmreclem1  14814  prmreclem2  14815  prmreclem3  14816  prmreclem5  14818  1arith  14825  elgz  14829  4sqlem13OLD  14855  4sqlem17OLD  14859  4sqlem18OLD  14860  4sqlem13  14861  4sqlem17  14865  4sqlem18  14866  vdwnnlem2  14900  vdwnnlem3  14901  ramtlecl  14905  isdrs  16121  istos  16223  islat  16235  isclat  16297  isdlat  16381  istsr  16405  issgrp  16470  ismnddef  16480  gsumvallem2  16561  isgrp  16619  elnmz  16798  gastacl  16905  gastacos  16906  symgfixelq  17016  psgneldm  17086  sylow1lem2  17177  sylow1lem4  17179  sylow2alem1  17195  sylow2alem2  17196  efgsdm  17306  iscmn  17363  iscyg  17440  iscyggen  17441  dprdw  17568  ablfacrplem  17624  ablfacrp  17625  ablfac1c  17630  ablfac1eu  17632  pgpfaclem1  17640  ablfaclem3  17646  ablfac2  17648  issrg  17667  isring  17710  iscrng  17713  isdrng  17905  islmod  18021  islvec  18253  lspsolvlem  18291  lbsextlem1  18307  lbsextlem3  18309  lbsextlem4  18310  islpir  18399  isnzr  18409  isrrg  18438  isdomn  18444  isassa  18465  psrbag  18514  psrbaglefi  18522  psrbagconcl  18523  psrbagconf1o  18524  gsumbagdiaglem  18525  mplelbas  18580  isphl  19117  pjdm  19192  ishil  19203  frlmssuvc1  19274  frlmssuvc2  19275  frlmsslsp  19276  gsummatr01lem1  19602  gsummatr01lem4  19605  gsummatr01  19606  mretopd  20030  neipeltop  20067  isperf  20089  ist0  20258  ist1  20259  ishaus  20260  iscnrm  20261  isreg  20270  isnrm  20273  ispnrm  20277  iscmp  20325  hauscmplem  20343  iscon  20350  concompss  20370  is1stc  20378  islly  20405  isnlly  20406  dfac14lem  20554  ishmeo  20696  ptcmplem3  20991  ptcmplem4  20992  istmd  21011  istgp  21014  tgpconcompeqg  21048  tgpt0  21055  qustgpopn  21056  istrg  21100  istdrg  21102  istlm  21121  istvc  21128  iscusp  21236  imasdsf1olem  21310  isxms  21384  isms  21386  blcld  21442  prdsxmslem2  21466  isngp  21532  isnrg  21585  isnlm  21600  icccmplem1  21742  icccmplem2  21743  isclm  21979  iscph  22032  isbn  22190  iscms  22197  ivthlem1  22274  ivthlem2  22275  ivthlem3  22276  elovolm  22297  ovolicc2lem2  22340  ovolicc2lem4  22342  ovolicc2lem5  22343  ismbl  22348  dyadmbllem  22425  dyadmbl  22426  ismbf1  22450  isi1f  22500  isibl  22591  isuc1p  22957  ismon1p  22959  radcnvle  23231  abelthlem2  23243  abelthlem7a  23248  atans  23712  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem5  23814  lgambdd  23818  wilthlem2  23850  wilthlem3  23851  ftalem3  23855  sqff1o  23963  dvdsmulf1o  23977  lgslem2  24079  lgslem3  24080  lgsfcl2  24084  rpvmasumlem  24179  dchrvmaeq0  24196  dchrisum0re  24205  pntlem3  24301  axcontlem2  24832  usgraidx2vlem1  24955  usgraidx2vlem2  24956  cusgraexi  25032  cusgrafilem2  25044  wlknwwlknfun  25274  wlknwwlkninj  25275  wlkiswwlkfun  25281  wlkiswwlkinj  25282  wlkiswwlksur  25283  wwlkextfun  25293  wwlkextinj  25294  wwlkextsur  25295  wwlkextproplem3  25307  clwwlkel  25357  clwwlkf  25358  clwwlkf1  25360  clwlkfclwwlk1hashn  25405  clwlkfoclwwlk  25409  clwlkf1clwwlklem1  25410  clwlkf1clwwlklem2  25411  clwlkf1clwwlklem3  25412  frgrawopreglem3  25610  extwwlkfab  25654  isablo  25847  iscbn  26342  hcau  26663  issh  26687  isch  26701  elcnop  27336  ellnop  27337  elbdop  27339  elhmop  27352  elcnfn  27361  ellnfn  27362  isst  27692  ishst  27693  ela  27818  isomnd  28293  isslmd  28347  isorng  28392  iscref  28501  isrrext  28634  ispisys  28804  isldsys  28808  isros  28820  issros  28827  oddpwdc  29004  eulerpartleme  29013  eulerpartlemo  29015  eulerpartlemd  29016  eulerpartlemt0  29019  eulerpartlemf  29020  eulerpartlemt  29021  eulerpartlemr  29024  eulerpartlemmf  29025  eulerpartlemgvv  29026  eulerpartlemgs2  29030  eulerpartlemn  29031  elprob  29059  ballotlemelo  29137  ballotleme  29146  bnj1152  29586  bnj1280  29608  subfacp1lem3  29684  subfacp1lem5  29686  erdszelem1  29693  ispcon  29725  isscon  29728  cvmsiota  29779  cvmlift2lem12  29816  rdgprc0  30218  elwlim  30284  neibastop1  30791  neibastop2lem  30792  neibastop2  30793  topdifinffinlem  31475  poimirlem5  31639  poimirlem6  31640  poimirlem7  31641  poimirlem8  31642  poimirlem10  31644  poimirlem11  31645  poimirlem12  31646  poimirlem15  31649  poimirlem16  31650  poimirlem17  31651  poimirlem18  31652  poimirlem19  31653  poimirlem20  31654  poimirlem21  31655  poimirlem22  31656  isprrngo  31977  toycom  32238  isopos  32445  isoml  32503  isatl  32564  iscvlat  32588  ishlat1  32617  cdlemm10N  34385  dihglblem2N  34561  lcfl1lem  34758  lcfls1lem  34801  mapdordlem1a  34901  mapdordlem1  34903  pellqrex  35423  islnm  35631  pwssplit4  35643  islnr  35666  hashgcdlem  35763  stoweidlem14  37433  stoweidlem16  37435  stoweidlem37  37457  stoweidlem48  37468  stoweidlem51  37471  stoweidlem59  37479  m1expevenALTV  38157  iseven2  38161  isodd3  38162  odd2np1ALTV  38183  opoeALTV  38192  opeoALTV  38193  isgbe  38232  isgbo  38233  isgboa  38234  usgedgvadf1lem1  38473  usgedgvadf1lem2  38474  usgedgvadf1ALTlem1  38476  usgedgvadf1ALTlem2  38477  0nodd  38558  1odd  38559  2nodd  38560  iscmgmALT  38608  issgrpALT  38609  iscsgrpALT  38610  isrng  38624  1neven  38680  2zlidl  38682  2zrngamgm  38687  2zrngagrp  38691  2zrngmmgm  38694  2zrngnmrid  38698
  Copyright terms: Public domain W3C validator