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

Theorem elrab2 3230
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 2499 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3228 . 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 1872   {crab 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082
This theorem is referenced by:  elrabsf  3338  pwnss  4589  fvmpti  5963  fvmptss2  5985  tfis  6695  elom  6709  oawordeulem  7266  oeeulem  7313  mapfienlem1  7927  mapfienlem3  7929  mapfien  7930  ordtypelem2  8043  ordtypelem3  8044  ordtypelem9  8050  wemapso2lem  8076  inf3lema  8138  oemapvali  8197  tz9.12lem3  8268  cofsmo  8706  enfin2i  8758  fin23lem28  8777  isf32lem6  8795  hsmexlem4  8866  zorn2lem2  8934  pwfseqlem1  9090  pwfseqlem3  9092  nqereu  9361  elz  10946  zsupss  11260  rpnnen1lem5  11301  elrp  11311  repos  11738  wwlktovf  13031  wwlktovf1  13032  wwlktovfo  13033  sqrlem1  13306  sqrlem2  13307  sqrlem6  13311  sqrlem7  13312  ello1  13578  elo1  13589  rlimrege0  13642  divalglem2  14372  divalglem2OLD  14373  divalglem4  14374  divalglem5OLD  14375  divalglem5  14376  divalglem9  14380  divalglem9OLD  14381  divalglem10  14382  bitsfzolem  14406  bitsfzolemOLD  14407  gcdcllem1  14472  gcdcllem2  14473  gcdcllem3  14474  bezoutlem1  14502  bezoutlem3OLD  14504  bezoutlem4OLD  14505  bezoutlem3  14507  bezoutlem4  14508  isprm  14623  maxprmfct  14651  phimullem  14726  eulerthlem1  14728  eulerthlem2  14729  pclem  14787  pcprecl  14788  pcprendvds  14789  infpn2  14856  prmreclem1  14859  prmreclem2  14860  prmreclem3  14861  prmreclem5  14863  1arith  14870  elgz  14874  4sqlem13OLD  14900  4sqlem17OLD  14904  4sqlem18OLD  14905  4sqlem13  14906  4sqlem17  14910  4sqlem18  14911  vdwnnlem2  14945  vdwnnlem3  14946  ramtlecl  14950  isdrs  16178  istos  16280  islat  16292  isclat  16354  isdlat  16438  istsr  16462  issgrp  16527  ismnddef  16537  gsumvallem2  16618  isgrp  16676  elnmz  16855  gastacl  16962  gastacos  16963  symgfixelq  17073  psgneldm  17143  sylow1lem2  17250  sylow1lem4  17252  sylow2alem1  17268  sylow2alem2  17269  efgsdm  17379  iscmn  17436  iscyg  17513  iscyggen  17514  dprdw  17641  ablfacrplem  17697  ablfacrp  17698  ablfac1c  17703  ablfac1eu  17705  pgpfaclem1  17713  ablfaclem3  17719  ablfac2  17721  issrg  17740  isring  17783  iscrng  17786  isdrng  17978  islmod  18094  islvec  18326  lspsolvlem  18364  lbsextlem1  18380  lbsextlem3  18382  lbsextlem4  18383  islpir  18472  isnzr  18482  isrrg  18511  isdomn  18517  isassa  18538  psrbag  18587  psrbaglefi  18595  psrbagconcl  18596  psrbagconf1o  18597  gsumbagdiaglem  18598  mplelbas  18653  isphl  19193  pjdm  19268  ishil  19279  frlmssuvc1  19350  frlmssuvc2  19351  frlmsslsp  19352  gsummatr01lem1  19678  gsummatr01lem4  19681  gsummatr01  19682  mretopd  20106  neipeltop  20143  isperf  20165  ist0  20334  ist1  20335  ishaus  20336  iscnrm  20337  isreg  20346  isnrm  20349  ispnrm  20353  iscmp  20401  hauscmplem  20419  iscon  20426  concompss  20446  is1stc  20454  islly  20481  isnlly  20482  dfac14lem  20630  ishmeo  20772  ptcmplem3  21067  ptcmplem4  21068  istmd  21087  istgp  21090  tgpconcompeqg  21124  tgpt0  21131  qustgpopn  21132  istrg  21176  istdrg  21178  istlm  21197  istvc  21204  iscusp  21312  imasdsf1olem  21386  isxms  21460  isms  21462  blcld  21518  prdsxmslem2  21542  isngp  21608  isnrg  21661  isnlm  21676  icccmplem1  21838  icccmplem2  21839  isclm  22093  iscph  22146  isbn  22304  iscms  22311  ivthlem1  22400  ivthlem2  22401  ivthlem3  22402  elovolm  22426  ovolicc2lem2  22469  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  ismbl  22478  dyadmbllem  22555  dyadmbl  22556  ismbf1  22580  isi1f  22630  isibl  22721  isuc1p  23089  ismon1p  23091  radcnvle  23373  abelthlem2  23385  abelthlem7a  23390  atans  23854  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem5  23956  lgambdd  23960  wilthlem2  23992  wilthlem3  23993  ftalem3  23997  sqff1o  24107  dvdsmulf1o  24121  lgslem2  24223  lgslem3  24224  lgsfcl2  24228  rpvmasumlem  24323  dchrvmaeq0  24340  dchrisum0re  24349  pntlem3  24445  axcontlem2  24993  usgraidx2vlem1  25116  usgraidx2vlem2  25117  cusgraexi  25194  cusgrafilem2  25206  wlknwwlknfun  25436  wlknwwlkninj  25437  wlkiswwlkfun  25443  wlkiswwlkinj  25444  wlkiswwlksur  25445  wwlkextfun  25455  wwlkextinj  25456  wwlkextsur  25457  wwlkextproplem3  25469  clwwlkel  25519  clwwlkf  25520  clwwlkf1  25522  clwlkfclwwlk1hashn  25567  clwlkfoclwwlk  25571  clwlkf1clwwlklem1  25572  clwlkf1clwwlklem2  25573  clwlkf1clwwlklem3  25574  frgrawopreglem3  25772  extwwlkfab  25816  isablo  26009  iscbn  26504  hcau  26835  issh  26859  isch  26873  elcnop  27508  ellnop  27509  elbdop  27511  elhmop  27524  elcnfn  27533  ellnfn  27534  isst  27864  ishst  27865  ela  27990  isomnd  28471  isslmd  28525  isorng  28570  iscref  28679  isrrext  28812  ispisys  28982  isldsys  28986  isros  28998  issros  29005  oddpwdc  29195  eulerpartleme  29204  eulerpartlemo  29206  eulerpartlemd  29207  eulerpartlemt0  29210  eulerpartlemf  29211  eulerpartlemt  29212  eulerpartlemr  29215  eulerpartlemmf  29216  eulerpartlemgvv  29217  eulerpartlemgs2  29221  eulerpartlemn  29222  elprob  29250  ballotlemelo  29328  ballotleme  29337  bnj1152  29815  bnj1280  29837  subfacp1lem3  29913  subfacp1lem5  29915  erdszelem1  29922  ispcon  29954  isscon  29957  cvmsiota  30008  cvmlift2lem12  30045  rdgprc0  30447  elwlim  30513  neibastop1  31020  neibastop2lem  31021  neibastop2  31022  topdifinffinlem  31714  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  isprrngo  32247  toycom  32508  isopos  32715  isoml  32773  isatl  32834  iscvlat  32858  ishlat1  32887  cdlemm10N  34655  dihglblem2N  34831  lcfl1lem  35028  lcfls1lem  35071  mapdordlem1a  35171  mapdordlem1  35173  pellqrex  35696  islnm  35905  pwssplit4  35917  islnr  35940  hashgcdlem  36044  stoweidlem14  37814  stoweidlem16  37816  stoweidlem37  37838  stoweidlem48  37849  stoweidlem51  37852  stoweidlem59  37860  ovn0lem  38291  m1expevenALTV  38647  iseven2  38651  isodd3  38652  odd2np1ALTV  38673  opoeALTV  38682  opeoALTV  38683  isgbe  38722  isgbo  38723  isgboa  38724  usgridx2vlem1  39085  usgridx2vlem2  39086  usgredgedga  39090  isfusgr  39152  nbumgrres  39202  iscusgr  39242  cusgrexi  39263  cusgrfilem2  39273  usgedgvadf1lem1  39344  usgedgvadf1lem2  39345  usgedgvadf1ALTlem1  39347  usgedgvadf1ALTlem2  39348  0nodd  39429  1odd  39430  2nodd  39431  iscmgmALT  39479  issgrpALT  39480  iscsgrpALT  39481  isrng  39495  1neven  39551  2zlidl  39553  2zrngamgm  39558  2zrngagrp  39562  2zrngmmgm  39565  2zrngnmrid  39569
  Copyright terms: Public domain W3C validator