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

Theorem ssrab2 3415
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 2701 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3414 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3365 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725   {cab 2416   {crab 2696    C_ wss 3307
This theorem is referenced by:  ssrabeq  3416  iinrab2  4141  riinrab  4153  rabexg  4340  pwnss  4352  frminex  4549  wereu2  4566  onminesb  4764  onminsb  4765  onintrab  4767  onnminsb  4770  onminex  4773  tfis  4820  omsson  4835  dmmptss  5352  ssimaex  5774  fnsuppres  5938  weniso  6061  canth  6525  riotacl  6550  riotassuni  6574  oawordeulem  6783  oeeulem  6830  nnawordex  6866  pmvalg  7015  fineqvlem  7309  ordtypelem2  7472  ordtypelem3  7473  ordtypelem4  7474  ordtypelem6  7476  hartogs  7497  wemapso2  7505  card2on  7506  wdom2d  7532  cantnfres  7617  oemapvali  7624  wemapwe  7638  tz9.12lem1  7697  tz9.12lem3  7699  rankf  7704  cplem1  7797  cardf2  7814  cardid2  7824  cardmin2  7869  acni3  7912  dfac2a  7994  cofsmo  8133  coftr  8137  fin2i2  8182  isfin2-2  8183  enfin2i  8185  fin23lem28  8204  fin23lem30  8206  isf32lem5  8221  isf32lem6  8222  isf32lem7  8223  isf32lem8  8224  fin1a2lem11  8274  fin1a2lem12  8275  hsmexlem4  8293  hsmexlem5  8294  hsmexlem6  8295  axdc3lem4  8317  ac6num  8343  ac6  8344  zorn2lem1  8360  zorn2lem3  8362  zorn2lem4  8363  zorn2lem5  8364  ondomon  8422  alephval2  8431  pwfseqlem1  8517  pwfseqlem3  8519  wunccl  8603  tskmcl  8700  0nnq  8785  elpqn  8786  infm3  9951  infmrcl  9971  uzf  10475  nnwos  10528  supminf  10547  zsupss  10549  rpnnen1lem1  10584  rpnnen1lem2  10585  rpnnen1lem3  10586  rpnnen1lem5  10588  rpre  10602  ixxf  10910  fzf  11031  flval3  11205  expge0  11399  expge1  11400  hashbclem  11684  sqrlem3  12033  sqrlem5  12035  rlimrege0  12356  incexc2  12601  divalglem2  12898  divalglem5  12900  divalglem8  12903  bitsf  12922  bitsfzolem  12929  sadadd2lem  12954  sadadd3  12956  sadcl  12957  smupf  12973  smuval2  12977  smupvallem  12978  smucl  12979  smueqlem  12985  gcdcllem3  12996  bezoutlem2  13022  bezoutlem3  13023  maxprmfct  13096  phicl2  13140  phibnd  13143  hashdvds  13147  phiprmpw  13148  phimullem  13151  eulerthlem2  13154  eulerth  13155  odzcllem  13161  odzdvds  13164  pclem  13195  infpn2  13264  prmreclem1  13267  prmreclem2  13268  prmreclem3  13269  prmreclem4  13270  prmreclem5  13271  4sqlem13  13308  4sqlem14  13309  4sqlem17  13312  4sqlem18  13313  vdwnnlem3  13348  hashbccl  13354  ramcl2lem  13360  ramtcl  13361  ramtcl2  13362  ramtub  13363  prdsds  13669  imasdsval2  13725  mrcflem  13814  isacs1i  13865  wunnat  14136  dmcoass  14204  lubid  14422  mhmeql  14747  gsumval1  14762  nmzsubg  14964  nmznsg  14967  conjnmz  15022  conjnmzb  15023  gastacl  15069  cntzval  15103  cntzssv  15110  odlem1  15156  odlem2  15160  odngen  15194  gexlem1  15196  gexlem2  15199  sylow1lem2  15216  sylow1lem3  15217  sylow1lem4  15218  sylow1lem5  15219  sylow2alem2  15235  sylow2a  15236  sylow2blem3  15239  sylow3lem2  15245  oddvdssubg  15453  cyggex2  15489  ablfacrplem  15606  ablfacrp2  15608  ablfac1eu  15614  pgpfaclem1  15622  ablfaclem2  15627  ablfaclem3  15628  lssacs  16026  lspf  16033  lspsolvlem  16197  lbsextlem2  16214  lbsextlem3  16215  lbsextlem4  16216  rrgeq0  16333  rrgss  16335  asplss  16371  aspsubrg  16373  psrbagconf1o  16422  psrass1lem  16425  psrdi  16453  psrdir  16454  psrass23  16456  resspsrmul  16463  mplbas  16476  mplbasss  16479  mplsubglem  16481  mplsubrglem  16485  mplmonmul  16510  psropprmul  16615  coe1mul2lem2  16644  cygznlem2a  16831  ocvfval  16876  ocvval  16877  fctop  17051  cctop  17053  ppttop  17054  epttop  17056  clscld  17094  mretopd  17139  neips  17160  neiptopnei  17179  ordtbaslem  17235  ordtuni  17237  ordtcld1  17244  ordtcld2  17245  cnpfval  17281  iscnp2  17286  cmpcov2  17436  cmpsublem  17445  tgcmp  17447  hauscmplem  17452  concompcld  17480  1stcfb  17491  2ndc1stc  17497  2ndcdisj  17502  kgentopon  17553  xkotf  17600  txkgen  17667  xkococnlem  17674  imastopn  17735  kqffn  17740  opnfbas  17857  flimfnfcls  18043  alexsubALT  18065  ptcmplem1  18066  ptcmplem2  18067  ptcmplem3  18068  symgtgp  18114  tgpconcompeqg  18124  tgpconcomp  18125  ghmcnp  18127  tsmsfbas  18140  eltsms  18145  utoptop  18247  utopbas  18248  imasdsf1olem  18386  blfvalps  18396  blfps  18419  blf  18420  blcld  18518  nmoffn  18728  nmofval  18731  nmogelb  18733  nmolb  18734  nmof  18736  icccmplem1  18836  icccmplem2  18837  icccmplem3  18838  ishtpy  18980  clsocv  19187  minveclem3b  19312  minveclem4  19316  ivthlem1  19331  ivthlem2  19332  ivthlem3  19333  ovolcl  19357  ovollb  19358  ovolgelb  19359  ovolge0  19360  ovolsslem  19363  ovolshftlem1  19388  ovolshft  19390  ovolscalem1  19392  ovolscalem2  19393  ovolsca  19394  ovolicc2lem3  19398  ovolicc2lem4  19399  ovolicc2lem5  19400  ovolicc2  19401  shftmbl  19416  iundisj  19425  dyadmax  19473  dyadmbllem  19474  dyadmbl  19475  opnmbllem  19476  iblmbf  19642  mdegmullem  19984  uc1pval  20045  mon1pval  20047  elqaalem1  20219  elqaalem3  20221  aannenlem2  20229  aalioulem2  20233  radcnvcl  20316  radcnvlt1  20317  radcnvle  20319  abelthlem4  20333  abelthlem6  20335  abelthlem9  20339  abelth  20340  atancn  20759  ftalem3  20840  ftalem4  20841  ftalem5  20842  efnnfsumcl  20868  isppw  20880  sgmval2  20909  efchtdvds  20925  sqff1o  20948  dvdsflip  20950  fsumdvdsdiaglem  20951  fsumdvdsdiag  20952  fsumdvdscom  20953  musum  20959  muinv  20961  dvdsmulf1o  20962  fsumdvdsmul  20963  sgmmul  20968  ppiub  20971  vmasum  20983  logfac2  20984  perfectlem2  20997  lgsfcl2  21069  lgsfcl  21071  lgscl  21077  lgseisenlem3  21118  lgseisenlem4  21119  lgsquadlem1  21121  lgsquadlem2  21122  rpvmasumlem  21164  rpvmasum2  21189  dchrisum0re  21190  dchrisum0lema  21191  dchrisum0lem1b  21192  dchrisum0lem1  21193  dchrisum0lem2a  21194  dchrisum0lem2  21195  dchrisum0lem3  21196  dchrisum0  21197  mudivsum  21207  mulogsum  21209  mulog2sumlem2  21212  vmalogdivsum2  21215  logsqvma  21219  logsqvma2  21220  selberglem3  21224  selberg  21225  selberg34r  21248  pntsval2  21253  pntrlog2bndlem1  21254  pntlem3  21286  umgrass  21337  umgran0  21338  umisuhgra  21345  usgrass  21367  usgrares1  21407  usgrafilem1  21408  nbgrassvt  21428  nbgraf1olem1  21434  cusgrares  21464  vdgrun  21655  vdgrfiun  21656  konigsberg  21692  ocsh  22768  spancl  22821  shsval2i  22872  ococin  22893  chsupid  22897  speccl  23385  atssch  23829  hatomistici  23848  chpssati  23849  iundisjf  24012  iundisjfi  24135  esumpinfval  24446  sigagensiga  24507  measvuni  24551  imambfm  24595  dya2iocuni  24616  ballotlemoex  24726  ballotlem2  24729  ballotlemfc0  24733  ballotlemfcc  24734  ballotlemfmpn  24735  ballotlemiex  24742  ballotlemsup  24745  ballotlem7  24776  ballotth  24778  lgamucov  24805  lgamucov2  24806  subfacp1lem3  24851  subfacp1lem5  24853  subfacp1lem6  24854  erdszelem2  24861  conpcon  24905  cvmliftmolem2  24952  cvmliftlem15  24968  cvmlift2lem12  24984  snmlff  24999  tfisg  25454  wfisg  25459  frinsg  25495  sltval2  25560  nodenselem4  25588  nobndlem5  25600  nofulllem5  25610  axcontlem2  25847  axcontlem7  25852  axcontlem8  25853  axcontlem10  25855  rankeq1o  26055  mblfinlem  26185  ismblfin  26188  mbfposadd  26195  cnambfre  26196  finminlem  26253  fnessref  26305  finlocfin  26311  neibastop1  26320  neibastop2lem  26321  cover2  26347  indexa  26367  fdc  26381  sstotbnd2  26415  sstotbnd3  26417  igenidl  26605  prnc  26609  mzpindd  26735  fiphp3d  26812  rencldnfilem  26813  irrapx1  26823  pellexlem3  26826  pellfundre  26876  pellfundge  26877  pellfundlb  26879  pellfundglb  26880  jm2.22  26998  jm2.23  26999  rpnnen3  27035  fglmod  27081  pwssplit4  27101  dsmmbase  27111  dsmmval2  27112  dsmmsubg  27119  frlmsslsp  27158  pwfi2f1o  27170  hbtlem6  27243  dgraalem  27260  dgraaub  27263  itgocn  27279  rgspncl  27284  issubmd  27293  symgsssg  27318  symgfisg  27319  psgnghm  27347  phisum  27428  stoweidlem14  27672  stoweidlem34  27692  stoweidlem44  27702  stoweidlem50  27708  stoweidlem51  27709  stoweidlem52  27710  stoweidlem57  27715  stoweidlem59  27717  frisusgranb  28143  frgrawopreg1  28195  frgrawopreg2  28196  bnj21  28834  bnj110  28981  bnj1204  29133  bnj1311  29145  toycom  29501  lkrlss  29624  atlatmstc  29848  atlatle  29849  glbconN  29905  linepsubN  30280  pmapssat  30287  pmaple  30289  pmapsub  30296  paddssat  30342  diass  31571  diaglbN  31584  diaintclN  31587  diassdvaN  31589  docaclN  31653  dibglbN  31695  dibintclN  31696  diclspsn  31723  dihglblem2N  31823  dih1dimatlem  31858  dihglb2  31871  dochval2  31881  dochcl  31882  dochvalr  31886  doch2val2  31893  dochss  31894  dochocss  31895  lclkr  32062  lclkrs  32068  lcdvbase  32122  lcdvbasess  32123  mapdunirnN  32179
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 2411
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 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rab 2701  df-in 3314  df-ss 3321
  Copyright terms: Public domain W3C validator