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

Theorem ssrab2 3420
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
ssrab2  |-  { x  e.  A  |  ph }  C_  A
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem ssrab2
StepHypRef Expression
1 df-rab 2706 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3419 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3370 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725   {cab 2421   {crab 2701    C_ wss 3312
This theorem is referenced by:  ssrabeq  3421  iinrab2  4146  riinrab  4158  rabexg  4345  pwnss  4357  frminex  4554  wereu2  4571  onminesb  4769  onminsb  4770  onintrab  4772  onnminsb  4775  onminex  4778  tfis  4825  omsson  4840  dmmptss  5357  ssimaex  5779  fnsuppres  5943  weniso  6066  canth  6530  riotacl  6555  riotassuni  6579  oawordeulem  6788  oeeulem  6835  nnawordex  6871  pmvalg  7020  fineqvlem  7314  ordtypelem2  7477  ordtypelem3  7478  ordtypelem4  7479  ordtypelem6  7481  hartogs  7502  wemapso2  7510  card2on  7511  wdom2d  7537  cantnfres  7622  oemapvali  7629  wemapwe  7643  tz9.12lem1  7702  tz9.12lem3  7704  rankf  7709  cplem1  7802  cardf2  7819  cardid2  7829  cardmin2  7874  acni3  7917  dfac2a  7999  cofsmo  8138  coftr  8142  fin2i2  8187  isfin2-2  8188  enfin2i  8190  fin23lem28  8209  fin23lem30  8211  isf32lem5  8226  isf32lem6  8227  isf32lem7  8228  isf32lem8  8229  fin1a2lem11  8279  fin1a2lem12  8280  hsmexlem4  8298  hsmexlem5  8299  hsmexlem6  8300  axdc3lem4  8322  ac6num  8348  ac6  8349  zorn2lem1  8365  zorn2lem3  8367  zorn2lem4  8368  zorn2lem5  8369  ondomon  8427  alephval2  8436  pwfseqlem1  8522  pwfseqlem3  8524  wunccl  8608  tskmcl  8705  0nnq  8790  elpqn  8791  infm3  9956  infmrcl  9976  uzf  10480  nnwos  10533  supminf  10552  zsupss  10554  rpnnen1lem1  10589  rpnnen1lem2  10590  rpnnen1lem3  10591  rpnnen1lem5  10593  rpre  10607  ixxf  10915  fzf  11036  flval3  11210  expge0  11404  expge1  11405  hashbclem  11689  sqrlem3  12038  sqrlem5  12040  rlimrege0  12361  incexc2  12606  divalglem2  12903  divalglem5  12905  divalglem8  12908  bitsf  12927  bitsfzolem  12934  sadadd2lem  12959  sadadd3  12961  sadcl  12962  smupf  12978  smuval2  12982  smupvallem  12983  smucl  12984  smueqlem  12990  gcdcllem3  13001  bezoutlem2  13027  bezoutlem3  13028  maxprmfct  13101  phicl2  13145  phibnd  13148  hashdvds  13152  phiprmpw  13153  phimullem  13156  eulerthlem2  13159  eulerth  13160  odzcllem  13166  odzdvds  13169  pclem  13200  infpn2  13269  prmreclem1  13272  prmreclem2  13273  prmreclem3  13274  prmreclem4  13275  prmreclem5  13276  4sqlem13  13313  4sqlem14  13314  4sqlem17  13317  4sqlem18  13318  vdwnnlem3  13353  hashbccl  13359  ramcl2lem  13365  ramtcl  13366  ramtcl2  13367  ramtub  13368  prdsds  13674  imasdsval2  13730  mrcflem  13819  isacs1i  13870  wunnat  14141  dmcoass  14209  lubid  14427  mhmeql  14752  gsumval1  14767  nmzsubg  14969  nmznsg  14972  conjnmz  15027  conjnmzb  15028  gastacl  15074  cntzval  15108  cntzssv  15115  odlem1  15161  odlem2  15165  odngen  15199  gexlem1  15201  gexlem2  15204  sylow1lem2  15221  sylow1lem3  15222  sylow1lem4  15223  sylow1lem5  15224  sylow2alem2  15240  sylow2a  15241  sylow2blem3  15244  sylow3lem2  15250  oddvdssubg  15458  cyggex2  15494  ablfacrplem  15611  ablfacrp2  15613  ablfac1eu  15619  pgpfaclem1  15627  ablfaclem2  15632  ablfaclem3  15633  lssacs  16031  lspf  16038  lspsolvlem  16202  lbsextlem2  16219  lbsextlem3  16220  lbsextlem4  16221  rrgeq0  16338  rrgss  16340  asplss  16376  aspsubrg  16378  psrbagconf1o  16427  psrass1lem  16430  psrdi  16458  psrdir  16459  psrass23  16461  resspsrmul  16468  mplbas  16481  mplbasss  16484  mplsubglem  16486  mplsubrglem  16490  mplmonmul  16515  psropprmul  16620  coe1mul2lem2  16649  cygznlem2a  16836  ocvfval  16881  ocvval  16882  fctop  17056  cctop  17058  ppttop  17059  epttop  17061  clscld  17099  mretopd  17144  neips  17165  neiptopnei  17184  ordtbaslem  17240  ordtuni  17242  ordtcld1  17249  ordtcld2  17250  cnpfval  17286  iscnp2  17291  cmpcov2  17441  cmpsublem  17450  tgcmp  17452  hauscmplem  17457  concompcld  17485  1stcfb  17496  2ndc1stc  17502  2ndcdisj  17507  kgentopon  17558  xkotf  17605  txkgen  17672  xkococnlem  17679  imastopn  17740  kqffn  17745  opnfbas  17862  flimfnfcls  18048  alexsubALT  18070  ptcmplem1  18071  ptcmplem2  18072  ptcmplem3  18073  symgtgp  18119  tgpconcompeqg  18129  tgpconcomp  18130  ghmcnp  18132  tsmsfbas  18145  eltsms  18150  utoptop  18252  utopbas  18253  imasdsf1olem  18391  blfvalps  18401  blfps  18424  blf  18425  blcld  18523  nmoffn  18733  nmofval  18736  nmogelb  18738  nmolb  18739  nmof  18741  icccmplem1  18841  icccmplem2  18842  icccmplem3  18843  ishtpy  18985  clsocv  19192  minveclem3b  19317  minveclem4  19321  ivthlem1  19336  ivthlem2  19337  ivthlem3  19338  ovolcl  19362  ovollb  19363  ovolgelb  19364  ovolge0  19365  ovolsslem  19368  ovolshftlem1  19393  ovolshft  19395  ovolscalem1  19397  ovolscalem2  19398  ovolsca  19399  ovolicc2lem3  19403  ovolicc2lem4  19404  ovolicc2lem5  19405  ovolicc2  19406  shftmbl  19421  iundisj  19430  dyadmax  19478  dyadmbllem  19479  dyadmbl  19480  opnmbllem  19481  iblmbf  19647  mdegmullem  19989  uc1pval  20050  mon1pval  20052  elqaalem1  20224  elqaalem3  20226  aannenlem2  20234  aalioulem2  20238  radcnvcl  20321  radcnvlt1  20322  radcnvle  20324  abelthlem4  20338  abelthlem6  20340  abelthlem9  20344  abelth  20345  atancn  20764  ftalem3  20845  ftalem4  20846  ftalem5  20847  efnnfsumcl  20873  isppw  20885  sgmval2  20914  efchtdvds  20930  sqff1o  20953  dvdsflip  20955  fsumdvdsdiaglem  20956  fsumdvdsdiag  20957  fsumdvdscom  20958  musum  20964  muinv  20966  dvdsmulf1o  20967  fsumdvdsmul  20968  sgmmul  20973  ppiub  20976  vmasum  20988  logfac2  20989  perfectlem2  21002  lgsfcl2  21074  lgsfcl  21076  lgscl  21082  lgseisenlem3  21123  lgseisenlem4  21124  lgsquadlem1  21126  lgsquadlem2  21127  rpvmasumlem  21169  rpvmasum2  21194  dchrisum0re  21195  dchrisum0lema  21196  dchrisum0lem1b  21197  dchrisum0lem1  21198  dchrisum0lem2a  21199  dchrisum0lem2  21200  dchrisum0lem3  21201  dchrisum0  21202  mudivsum  21212  mulogsum  21214  mulog2sumlem2  21217  vmalogdivsum2  21220  logsqvma  21224  logsqvma2  21225  selberglem3  21229  selberg  21230  selberg34r  21253  pntsval2  21258  pntrlog2bndlem1  21259  pntlem3  21291  umgrass  21342  umgran0  21343  umisuhgra  21350  usgrass  21372  usgrares1  21412  usgrafilem1  21413  nbgrassvt  21433  nbgraf1olem1  21439  cusgrares  21469  vdgrun  21660  vdgrfiun  21661  konigsberg  21697  ocsh  22773  spancl  22826  shsval2i  22877  ococin  22898  chsupid  22902  speccl  23390  atssch  23834  hatomistici  23853  chpssati  23854  iundisjf  24017  iundisjfi  24140  esumpinfval  24451  sigagensiga  24512  measvuni  24556  imambfm  24600  dya2iocuni  24621  ballotlemoex  24731  ballotlem2  24734  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemfmpn  24740  ballotlemiex  24747  ballotlemsup  24750  ballotlem7  24781  ballotth  24783  lgamucov  24810  lgamucov2  24811  subfacp1lem3  24856  subfacp1lem5  24858  subfacp1lem6  24859  erdszelem2  24866  conpcon  24910  cvmliftmolem2  24957  cvmliftlem15  24973  cvmlift2lem12  24989  snmlff  25004  tfisg  25459  wfisg  25464  frinsg  25500  sltval2  25565  nodenselem4  25593  nobndlem5  25605  nofulllem5  25615  axcontlem2  25852  axcontlem7  25857  axcontlem8  25858  axcontlem10  25860  rankeq1o  26060  mblfinlem  26190  ismblfin  26193  mbfposadd  26200  cnambfre  26201  finminlem  26258  fnessref  26310  finlocfin  26316  neibastop1  26325  neibastop2lem  26326  cover2  26352  indexa  26372  fdc  26386  sstotbnd2  26420  sstotbnd3  26422  igenidl  26610  prnc  26614  mzpindd  26740  fiphp3d  26817  rencldnfilem  26818  irrapx1  26828  pellexlem3  26831  pellfundre  26881  pellfundge  26882  pellfundlb  26884  pellfundglb  26885  jm2.22  27003  jm2.23  27004  rpnnen3  27040  fglmod  27086  pwssplit4  27106  dsmmbase  27116  dsmmval2  27117  dsmmsubg  27124  frlmsslsp  27163  pwfi2f1o  27175  hbtlem6  27248  dgraalem  27265  dgraaub  27268  itgocn  27284  rgspncl  27289  issubmd  27298  symgsssg  27323  symgfisg  27324  psgnghm  27352  phisum  27433  stoweidlem14  27677  stoweidlem34  27697  stoweidlem44  27707  stoweidlem50  27713  stoweidlem51  27714  stoweidlem52  27715  stoweidlem57  27720  stoweidlem59  27722  frisusgranb  28245  frgrawopreg1  28297  frgrawopreg2  28298  bnj21  28936  bnj110  29083  bnj1204  29235  bnj1311  29247  toycom  29609  lkrlss  29732  atlatmstc  29956  atlatle  29957  glbconN  30013  linepsubN  30388  pmapssat  30395  pmaple  30397  pmapsub  30404  paddssat  30450  diass  31679  diaglbN  31692  diaintclN  31695  diassdvaN  31697  docaclN  31761  dibglbN  31803  dibintclN  31804  diclspsn  31831  dihglblem2N  31931  dih1dimatlem  31966  dihglb2  31979  dochval2  31989  dochcl  31990  dochvalr  31994  doch2val2  32001  dochss  32002  dochocss  32003  lclkr  32170  lclkrs  32176  lcdvbase  32230  lcdvbasess  32231  mapdunirnN  32287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator