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

Theorem elrab2 3184
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 2460 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3182 . 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 367    = wceq 1399    e. wcel 1826   {crab 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036
This theorem is referenced by:  elrabsf  3291  pwnss  4530  fvmpti  5856  fvmptss2  5877  tfis  6588  elom  6602  oawordeulem  7121  oeeulem  7168  mapfienlem1  7779  mapfienlem3  7781  mapfien  7782  ordtypelem2  7859  ordtypelem3  7860  ordtypelem9  7866  wemapso2OLD  7892  wemapso2lem  7893  inf3lema  7955  oemapvali  8016  mapfienOLD  8051  tz9.12lem3  8120  cofsmo  8562  enfin2i  8614  fin23lem28  8633  isf32lem6  8651  hsmexlem4  8722  zorn2lem2  8790  pwfseqlem1  8947  pwfseqlem3  8949  nqereu  9218  elz  10783  zsupss  11090  rpnnen1lem5  11131  elrp  11141  repos  11542  wwlktovf  12805  wwlktovf1  12806  wwlktovfo  12807  sqrlem1  13078  sqrlem2  13079  sqrlem6  13083  sqrlem7  13084  ello1  13340  elo1  13351  rlimrege0  13404  divalglem2  14055  divalglem4  14056  divalglem5  14057  divalglem9  14061  divalglem10  14062  bitsfzolem  14086  gcdcllem1  14151  gcdcllem2  14152  gcdcllem3  14153  bezoutlem1  14178  bezoutlem3  14180  bezoutlem4  14181  isprm  14221  maxprmfct  14256  phimullem  14311  eulerthlem1  14313  eulerthlem2  14314  pclem  14364  pcprecl  14365  pcprendvds  14366  infpn2  14433  prmreclem1  14436  prmreclem2  14437  prmreclem3  14438  prmreclem5  14440  1arith  14447  elgz  14451  4sqlem13  14477  4sqlem17  14481  4sqlem18  14482  vdwnnlem2  14516  vdwnnlem3  14517  ramtlecl  14520  isdrs  15680  istos  15782  islat  15794  isclat  15856  isdlat  15940  istsr  15964  issgrp  16029  ismnddef  16039  gsumvallem2  16120  isgrp  16178  elnmz  16357  gastacl  16464  gastacos  16465  symgfixelq  16575  psgneldm  16645  sylow1lem2  16736  sylow1lem4  16738  sylow2alem1  16754  sylow2alem2  16755  efgsdm  16865  iscmn  16922  iscyg  16999  iscyggen  17000  dprdw  17156  dprdwOLD  17163  ablfacrplem  17229  ablfacrp  17230  ablfac1c  17235  ablfac1eu  17237  pgpfaclem1  17245  ablfaclem3  17251  ablfac2  17253  issrg  17272  isring  17315  iscrng  17318  isdrng  17513  islmod  17629  islvec  17863  lspsolvlem  17901  lbsextlem1  17917  lbsextlem3  17919  lbsextlem4  17920  islpir  18010  isnzr  18020  isrrg  18049  isdomn  18056  isassa  18077  psrbag  18126  psrbaglefi  18136  psrbaglefiOLD  18137  psrbagconcl  18138  psrbagconf1o  18139  gsumbagdiaglem  18140  mplelbas  18200  mplelbasOLD  18202  isphl  18754  pjdm  18829  ishil  18840  frlmssuvc1  18914  frlmssuvc2  18915  frlmsslsp  18916  gsummatr01lem1  19242  gsummatr01lem4  19245  gsummatr01  19246  mretopd  19679  neipeltop  19716  isperf  19738  ist0  19907  ist1  19908  ishaus  19909  iscnrm  19910  isreg  19919  isnrm  19922  ispnrm  19926  iscmp  19974  hauscmplem  19992  iscon  19999  concompss  20019  is1stc  20027  islly  20054  isnlly  20055  dfac14lem  20203  ishmeo  20345  ptcmplem3  20639  ptcmplem4  20640  istmd  20658  istgp  20661  tgpconcompeqg  20695  tgpt0  20702  qustgpopn  20703  istrg  20751  istdrg  20753  istlm  20772  istvc  20779  iscusp  20887  imasdsf1olem  20961  isxms  21035  isms  21037  blcld  21093  prdsxmslem2  21117  isngp  21201  isnrg  21254  isnlm  21269  icccmplem1  21412  icccmplem2  21413  isclm  21649  iscph  21702  isbn  21862  iscms  21869  ivthlem1  21948  ivthlem2  21949  ivthlem3  21950  elovolm  21971  ovolicc2lem2  22014  ovolicc2lem4  22016  ovolicc2lem5  22017  ismbl  22022  dyadmbllem  22093  dyadmbl  22094  ismbf1  22118  isi1f  22166  isibl  22257  isuc1p  22626  ismon1p  22628  radcnvle  22900  abelthlem2  22912  abelthlem7a  22917  atans  23377  wilthlem2  23460  wilthlem3  23461  ftalem3  23465  sqff1o  23573  dvdsmulf1o  23587  lgslem2  23689  lgslem3  23690  lgsfcl2  23694  rpvmasumlem  23789  dchrvmaeq0  23806  dchrisum0re  23815  pntlem3  23911  axcontlem2  24389  usgraidx2vlem1  24512  usgraidx2vlem2  24513  cusgraexi  24589  cusgrafilem2  24601  wlknwwlknfun  24831  wlknwwlkninj  24832  wlkiswwlkfun  24838  wlkiswwlkinj  24839  wlkiswwlksur  24840  wwlkextfun  24850  wwlkextinj  24851  wwlkextsur  24852  wwlkextproplem3  24864  clwwlkel  24914  clwwlkf  24915  clwwlkf1  24917  clwlkfclwwlk1hashn  24962  clwlkfoclwwlk  24966  clwlkf1clwwlklem1  24967  clwlkf1clwwlklem2  24968  clwlkf1clwwlklem3  24969  frgrawopreglem3  25167  extwwlkfab  25211  isablo  25402  iscbn  25897  hcau  26218  issh  26242  isch  26257  elcnop  26892  ellnop  26893  elbdop  26895  elhmop  26908  elcnfn  26917  ellnfn  26918  isst  27248  ishst  27249  ela  27374  isomnd  27844  isslmd  27898  isorng  27943  iscref  28001  isrrext  28134  ispisys  28301  isldsys  28304  oddpwdc  28476  eulerpartleme  28485  eulerpartlemo  28487  eulerpartlemd  28488  eulerpartlemt0  28491  eulerpartlemf  28492  eulerpartlemt  28493  eulerpartlemr  28496  eulerpartlemmf  28497  eulerpartlemgvv  28498  eulerpartlemgs2  28502  eulerpartlemn  28503  elprob  28531  ballotlemelo  28609  ballotleme  28618  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem5  28764  lgambdd  28768  subfacp1lem3  28815  subfacp1lem5  28817  erdszelem1  28824  ispcon  28857  isscon  28860  cvmsiota  28911  cvmlift2lem12  28948  rdgprc0  29391  elwlim  29544  neibastop1  30343  neibastop2lem  30344  neibastop2  30345  isprrngo  30613  pellqrex  30980  islnm  31189  pwssplit4  31201  islnr  31228  hashgcdlem  31325  stoweidlem14  31962  stoweidlem16  31964  stoweidlem37  31985  stoweidlem48  31996  stoweidlem51  31999  stoweidlem59  32007  m1expevenALTV  32490  iseven2  32494  isodd3  32495  odd2np1ALTV  32516  opoeALTV  32525  opeoALTV  32526  usgedgvadf1lem1  32731  usgedgvadf1lem2  32732  usgedgvadf1ALTlem1  32734  usgedgvadf1ALTlem2  32735  0nodd  32816  1odd  32817  2nodd  32818  iscmgmALT  32866  issgrpALT  32867  iscsgrpALT  32868  isrng  32882  1neven  32938  2zlidl  32940  2zrngamgm  32945  2zrngagrp  32949  2zrngmmgm  32952  2zrngnmrid  32956  bnj1152  34401  bnj1280  34423  toycom  35111  isopos  35318  isoml  35376  isatl  35437  iscvlat  35461  ishlat1  35490  cdlemm10N  37258  dihglblem2N  37434  lcfl1lem  37631  lcfls1lem  37674  mapdordlem1a  37774  mapdordlem1  37776
  Copyright terms: Public domain W3C validator