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

Theorem ssrab2 3364
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 2651 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3363 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3314 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1717   {cab 2366   {crab 2646    C_ wss 3256
This theorem is referenced by:  ssrabeq  3365  iinrab2  4088  riinrab  4100  rabexg  4287  pwnss  4299  frminex  4496  wereu2  4513  onminesb  4711  onminsb  4712  onintrab  4714  onnminsb  4717  onminex  4720  tfis  4767  omsson  4782  dmmptss  5299  ssimaex  5720  fnsuppres  5884  weniso  6007  canth  6468  riotacl  6493  riotassuni  6517  oawordeulem  6726  oeeulem  6773  nnawordex  6809  pmvalg  6958  fineqvlem  7252  ordtypelem2  7414  ordtypelem3  7415  ordtypelem4  7416  ordtypelem6  7418  hartogs  7439  wemapso2  7447  card2on  7448  wdom2d  7474  cantnfres  7559  oemapvali  7566  wemapwe  7580  tz9.12lem1  7639  tz9.12lem3  7641  rankf  7646  cplem1  7739  cardf2  7756  cardid2  7766  cardmin2  7811  acni3  7854  dfac2a  7936  cofsmo  8075  coftr  8079  fin2i2  8124  isfin2-2  8125  enfin2i  8127  fin23lem28  8146  fin23lem30  8148  isf32lem5  8163  isf32lem6  8164  isf32lem7  8165  isf32lem8  8166  fin1a2lem11  8216  fin1a2lem12  8217  hsmexlem4  8235  hsmexlem5  8236  hsmexlem6  8237  axdc3lem4  8259  ac6num  8285  ac6  8286  zorn2lem1  8302  zorn2lem3  8304  zorn2lem4  8305  zorn2lem5  8306  ondomon  8364  alephval2  8373  pwfseqlem1  8459  pwfseqlem3  8461  wunccl  8545  tskmcl  8642  0nnq  8727  elpqn  8728  infm3  9892  infmrcl  9912  uzf  10416  nnwos  10469  supminf  10488  zsupss  10490  rpnnen1lem1  10525  rpnnen1lem2  10526  rpnnen1lem3  10527  rpnnen1lem5  10529  rpre  10543  ixxf  10851  fzf  10972  flval3  11142  expge0  11336  expge1  11337  hashbclem  11621  sqrlem3  11970  sqrlem5  11972  rlimrege0  12293  incexc2  12538  divalglem2  12835  divalglem5  12837  divalglem8  12840  bitsf  12859  bitsfzolem  12866  sadadd2lem  12891  sadadd3  12893  sadcl  12894  smupf  12910  smuval2  12914  smupvallem  12915  smucl  12916  smueqlem  12922  gcdcllem3  12933  bezoutlem2  12959  bezoutlem3  12960  maxprmfct  13033  phicl2  13077  phibnd  13080  hashdvds  13084  phiprmpw  13085  phimullem  13088  eulerthlem2  13091  eulerth  13092  odzcllem  13098  odzdvds  13101  pclem  13132  infpn2  13201  prmreclem1  13204  prmreclem2  13205  prmreclem3  13206  prmreclem4  13207  prmreclem5  13208  4sqlem13  13245  4sqlem14  13246  4sqlem17  13249  4sqlem18  13250  vdwnnlem3  13285  hashbccl  13291  ramcl2lem  13297  ramtcl  13298  ramtcl2  13299  ramtub  13300  prdsds  13606  imasdsval2  13662  mrcflem  13751  isacs1i  13802  wunnat  14073  dmcoass  14141  lubid  14359  mhmeql  14684  gsumval1  14699  nmzsubg  14901  nmznsg  14904  conjnmz  14959  conjnmzb  14960  gastacl  15006  cntzval  15040  cntzssv  15047  odlem1  15093  odlem2  15097  odngen  15131  gexlem1  15133  gexlem2  15136  sylow1lem2  15153  sylow1lem3  15154  sylow1lem4  15155  sylow1lem5  15156  sylow2alem2  15172  sylow2a  15173  sylow2blem3  15176  sylow3lem2  15182  oddvdssubg  15390  cyggex2  15426  ablfacrplem  15543  ablfacrp2  15545  ablfac1eu  15551  pgpfaclem1  15559  ablfaclem2  15564  ablfaclem3  15565  lssacs  15963  lspf  15970  lspsolvlem  16134  lbsextlem2  16151  lbsextlem3  16152  lbsextlem4  16153  rrgeq0  16270  rrgss  16272  asplss  16308  aspsubrg  16310  psrbagconf1o  16359  psrass1lem  16362  psrdi  16390  psrdir  16391  psrass23  16393  resspsrmul  16400  mplbas  16413  mplbasss  16416  mplsubglem  16418  mplsubrglem  16422  mplmonmul  16447  psropprmul  16552  coe1mul2lem2  16581  cygznlem2a  16764  ocvfval  16809  ocvval  16810  fctop  16984  cctop  16986  ppttop  16987  epttop  16989  clscld  17027  mretopd  17072  neips  17093  neiptopnei  17112  ordtbaslem  17167  ordtuni  17169  ordtcld1  17176  ordtcld2  17177  cnpfval  17213  iscnp2  17218  cmpcov2  17368  cmpsublem  17377  tgcmp  17379  hauscmplem  17384  concompcld  17411  1stcfb  17422  2ndc1stc  17428  2ndcdisj  17433  kgentopon  17484  xkotf  17531  txkgen  17598  xkococnlem  17605  imastopn  17666  kqffn  17671  opnfbas  17788  flimfnfcls  17974  alexsubALT  17996  ptcmplem1  17997  ptcmplem2  17998  ptcmplem3  17999  symgtgp  18045  tgpconcompeqg  18055  tgpconcomp  18056  ghmcnp  18058  tsmsfbas  18071  eltsms  18076  utoptop  18178  utopbas  18179  imasdsf1olem  18304  blfval  18314  blf  18328  blcld  18418  nmoffn  18609  nmofval  18612  nmogelb  18614  nmolb  18615  nmof  18617  icccmplem1  18717  icccmplem2  18718  icccmplem3  18719  ishtpy  18861  clsocv  19068  minveclem3b  19189  minveclem4  19193  ivthlem1  19208  ivthlem2  19209  ivthlem3  19210  ovolcl  19234  ovollb  19235  ovolgelb  19236  ovolge0  19237  ovolsslem  19240  ovolshftlem1  19265  ovolshft  19267  ovolscalem1  19269  ovolscalem2  19270  ovolsca  19271  ovolicc2lem3  19275  ovolicc2lem4  19276  ovolicc2lem5  19277  ovolicc2  19278  shftmbl  19293  iundisj  19302  dyadmax  19350  dyadmbllem  19351  dyadmbl  19352  opnmbllem  19353  iblmbf  19519  mdegmullem  19861  uc1pval  19922  mon1pval  19924  elqaalem1  20096  elqaalem3  20098  aannenlem2  20106  aalioulem2  20110  radcnvcl  20193  radcnvlt1  20194  radcnvle  20196  abelthlem4  20210  abelthlem6  20212  abelthlem9  20216  abelth  20217  atancn  20636  ftalem3  20717  ftalem4  20718  ftalem5  20719  efnnfsumcl  20745  isppw  20757  sgmval2  20786  efchtdvds  20802  sqff1o  20825  dvdsflip  20827  fsumdvdsdiaglem  20828  fsumdvdsdiag  20829  fsumdvdscom  20830  musum  20836  muinv  20838  dvdsmulf1o  20839  fsumdvdsmul  20840  sgmmul  20845  ppiub  20848  vmasum  20860  logfac2  20861  perfectlem2  20874  lgsfcl2  20946  lgsfcl  20948  lgscl  20954  lgseisenlem3  20995  lgseisenlem4  20996  lgsquadlem1  20998  lgsquadlem2  20999  rpvmasumlem  21041  rpvmasum2  21066  dchrisum0re  21067  dchrisum0lema  21068  dchrisum0lem1b  21069  dchrisum0lem1  21070  dchrisum0lem2a  21071  dchrisum0lem2  21072  dchrisum0lem3  21073  dchrisum0  21074  mudivsum  21084  mulogsum  21086  mulog2sumlem2  21089  vmalogdivsum2  21092  logsqvma  21096  logsqvma2  21097  selberglem3  21101  selberg  21102  selberg34r  21125  pntsval2  21130  pntrlog2bndlem1  21131  pntlem3  21163  umgrass  21214  umgran0  21215  umisuhgra  21222  usgrass  21244  usgrares1  21283  usgrafilem1  21284  nbgrassvt  21304  nbgraf1olem1  21310  cusgrares  21340  vdgrun  21513  vdgrfiun  21514  konigsberg  21550  ocsh  22626  spancl  22679  shsval2i  22730  ococin  22751  chsupid  22755  speccl  23243  atssch  23687  hatomistici  23706  chpssati  23707  iundisjf  23865  iundisjfi  23983  esumpinfval  24252  sigagensiga  24313  measvuni  24355  imambfm  24399  dya2iocuni  24420  ballotlemoex  24515  ballotlem2  24518  ballotlemfc0  24522  ballotlemfcc  24523  ballotlemfmpn  24524  ballotlemiex  24531  ballotlemsup  24534  ballotlem7  24565  ballotth  24567  lgamucov  24594  lgamucov2  24595  subfacp1lem3  24640  subfacp1lem5  24642  subfacp1lem6  24643  erdszelem2  24650  conpcon  24694  cvmliftmolem2  24741  cvmliftlem15  24757  cvmlift2lem12  24773  snmlff  24788  tfisg  25221  wfisg  25226  frinsg  25262  sltval2  25327  nodenselem4  25355  nobndlem5  25367  nofulllem5  25377  axcontlem2  25611  axcontlem7  25616  axcontlem8  25617  axcontlem10  25619  rankeq1o  25819  itgaddnclem2  25957  finminlem  26005  fnessref  26057  finlocfin  26063  neibastop1  26072  neibastop2lem  26073  cover2  26099  indexa  26119  fdc  26133  sstotbnd2  26167  sstotbnd3  26169  igenidl  26357  prnc  26361  mzpindd  26487  fiphp3d  26564  rencldnfilem  26565  irrapx1  26575  pellexlem3  26578  pellfundre  26628  pellfundge  26629  pellfundlb  26631  pellfundglb  26632  jm2.22  26750  jm2.23  26751  rpnnen3  26787  fglmod  26833  pwssplit4  26853  dsmmbase  26863  dsmmval2  26864  dsmmsubg  26871  frlmsslsp  26910  pwfi2f1o  26922  hbtlem6  26995  dgraalem  27012  dgraaub  27015  itgocn  27031  rgspncl  27036  issubmd  27045  symgsssg  27070  symgfisg  27071  psgnghm  27099  phisum  27180  stoweidlem14  27424  stoweidlem34  27444  stoweidlem44  27454  stoweidlem50  27460  stoweidlem51  27461  stoweidlem52  27462  stoweidlem57  27467  stoweidlem59  27469  frisusgranb  27743  frgrawopreg1  27795  frgrawopreg2  27796  bnj21  28413  bnj110  28560  bnj1204  28712  bnj1311  28724  toycom  29138  lkrlss  29261  atlatmstc  29485  atlatle  29486  glbconN  29542  linepsubN  29917  pmapssat  29924  pmaple  29926  pmapsub  29933  paddssat  29979  diass  31208  diaglbN  31221  diaintclN  31224  diassdvaN  31226  docaclN  31290  dibglbN  31332  dibintclN  31333  diclspsn  31360  dihglblem2N  31460  dih1dimatlem  31495  dihglb2  31508  dochval2  31518  dochcl  31519  dochvalr  31523  doch2val2  31530  dochss  31531  dochocss  31532  lclkr  31699  lclkrs  31705  lcdvbase  31759  lcdvbasess  31760  mapdunirnN  31816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator