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

Theorem ssrab2 3388
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 2675 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3387 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3338 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1721   {cab 2390   {crab 2670    C_ wss 3280
This theorem is referenced by:  ssrabeq  3389  iinrab2  4114  riinrab  4126  rabexg  4313  pwnss  4325  frminex  4522  wereu2  4539  onminesb  4737  onminsb  4738  onintrab  4740  onnminsb  4743  onminex  4746  tfis  4793  omsson  4808  dmmptss  5325  ssimaex  5747  fnsuppres  5911  weniso  6034  canth  6498  riotacl  6523  riotassuni  6547  oawordeulem  6756  oeeulem  6803  nnawordex  6839  pmvalg  6988  fineqvlem  7282  ordtypelem2  7444  ordtypelem3  7445  ordtypelem4  7446  ordtypelem6  7448  hartogs  7469  wemapso2  7477  card2on  7478  wdom2d  7504  cantnfres  7589  oemapvali  7596  wemapwe  7610  tz9.12lem1  7669  tz9.12lem3  7671  rankf  7676  cplem1  7769  cardf2  7786  cardid2  7796  cardmin2  7841  acni3  7884  dfac2a  7966  cofsmo  8105  coftr  8109  fin2i2  8154  isfin2-2  8155  enfin2i  8157  fin23lem28  8176  fin23lem30  8178  isf32lem5  8193  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  fin1a2lem11  8246  fin1a2lem12  8247  hsmexlem4  8265  hsmexlem5  8266  hsmexlem6  8267  axdc3lem4  8289  ac6num  8315  ac6  8316  zorn2lem1  8332  zorn2lem3  8334  zorn2lem4  8335  zorn2lem5  8336  ondomon  8394  alephval2  8403  pwfseqlem1  8489  pwfseqlem3  8491  wunccl  8575  tskmcl  8672  0nnq  8757  elpqn  8758  infm3  9923  infmrcl  9943  uzf  10447  nnwos  10500  supminf  10519  zsupss  10521  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  rpre  10574  ixxf  10882  fzf  11003  flval3  11177  expge0  11371  expge1  11372  hashbclem  11656  sqrlem3  12005  sqrlem5  12007  rlimrege0  12328  incexc2  12573  divalglem2  12870  divalglem5  12872  divalglem8  12875  bitsf  12894  bitsfzolem  12901  sadadd2lem  12926  sadadd3  12928  sadcl  12929  smupf  12945  smuval2  12949  smupvallem  12950  smucl  12951  smueqlem  12957  gcdcllem3  12968  bezoutlem2  12994  bezoutlem3  12995  maxprmfct  13068  phicl2  13112  phibnd  13115  hashdvds  13119  phiprmpw  13120  phimullem  13123  eulerthlem2  13126  eulerth  13127  odzcllem  13133  odzdvds  13136  pclem  13167  infpn2  13236  prmreclem1  13239  prmreclem2  13240  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  4sqlem13  13280  4sqlem14  13281  4sqlem17  13284  4sqlem18  13285  vdwnnlem3  13320  hashbccl  13326  ramcl2lem  13332  ramtcl  13333  ramtcl2  13334  ramtub  13335  prdsds  13641  imasdsval2  13697  mrcflem  13786  isacs1i  13837  wunnat  14108  dmcoass  14176  lubid  14394  mhmeql  14719  gsumval1  14734  nmzsubg  14936  nmznsg  14939  conjnmz  14994  conjnmzb  14995  gastacl  15041  cntzval  15075  cntzssv  15082  odlem1  15128  odlem2  15132  odngen  15166  gexlem1  15168  gexlem2  15171  sylow1lem2  15188  sylow1lem3  15189  sylow1lem4  15190  sylow1lem5  15191  sylow2alem2  15207  sylow2a  15208  sylow2blem3  15211  sylow3lem2  15217  oddvdssubg  15425  cyggex2  15461  ablfacrplem  15578  ablfacrp2  15580  ablfac1eu  15586  pgpfaclem1  15594  ablfaclem2  15599  ablfaclem3  15600  lssacs  15998  lspf  16005  lspsolvlem  16169  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  rrgeq0  16305  rrgss  16307  asplss  16343  aspsubrg  16345  psrbagconf1o  16394  psrass1lem  16397  psrdi  16425  psrdir  16426  psrass23  16428  resspsrmul  16435  mplbas  16448  mplbasss  16451  mplsubglem  16453  mplsubrglem  16457  mplmonmul  16482  psropprmul  16587  coe1mul2lem2  16616  cygznlem2a  16803  ocvfval  16848  ocvval  16849  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  clscld  17066  mretopd  17111  neips  17132  neiptopnei  17151  ordtbaslem  17206  ordtuni  17208  ordtcld1  17215  ordtcld2  17216  cnpfval  17252  iscnp2  17257  cmpcov2  17407  cmpsublem  17416  tgcmp  17418  hauscmplem  17423  concompcld  17450  1stcfb  17461  2ndc1stc  17467  2ndcdisj  17472  kgentopon  17523  xkotf  17570  txkgen  17637  xkococnlem  17644  imastopn  17705  kqffn  17710  opnfbas  17827  flimfnfcls  18013  alexsubALT  18035  ptcmplem1  18036  ptcmplem2  18037  ptcmplem3  18038  symgtgp  18084  tgpconcompeqg  18094  tgpconcomp  18095  ghmcnp  18097  tsmsfbas  18110  eltsms  18115  utoptop  18217  utopbas  18218  imasdsf1olem  18356  blfvalps  18366  blfps  18389  blf  18390  blcld  18488  nmoffn  18698  nmofval  18701  nmogelb  18703  nmolb  18704  nmof  18706  icccmplem1  18806  icccmplem2  18807  icccmplem3  18808  ishtpy  18950  clsocv  19157  minveclem3b  19282  minveclem4  19286  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ovolcl  19327  ovollb  19328  ovolgelb  19329  ovolge0  19330  ovolsslem  19333  ovolshftlem1  19358  ovolshft  19360  ovolscalem1  19362  ovolscalem2  19363  ovolsca  19364  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicc2  19371  shftmbl  19386  iundisj  19395  dyadmax  19443  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  iblmbf  19612  mdegmullem  19954  uc1pval  20015  mon1pval  20017  elqaalem1  20189  elqaalem3  20191  aannenlem2  20199  aalioulem2  20203  radcnvcl  20286  radcnvlt1  20287  radcnvle  20289  abelthlem4  20303  abelthlem6  20305  abelthlem9  20309  abelth  20310  atancn  20729  ftalem3  20810  ftalem4  20811  ftalem5  20812  efnnfsumcl  20838  isppw  20850  sgmval2  20879  efchtdvds  20895  sqff1o  20918  dvdsflip  20920  fsumdvdsdiaglem  20921  fsumdvdsdiag  20922  fsumdvdscom  20923  musum  20929  muinv  20931  dvdsmulf1o  20932  fsumdvdsmul  20933  sgmmul  20938  ppiub  20941  vmasum  20953  logfac2  20954  perfectlem2  20967  lgsfcl2  21039  lgsfcl  21041  lgscl  21047  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  rpvmasumlem  21134  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrisum0  21167  mudivsum  21177  mulogsum  21179  mulog2sumlem2  21182  vmalogdivsum2  21185  logsqvma  21189  logsqvma2  21190  selberglem3  21194  selberg  21195  selberg34r  21218  pntsval2  21223  pntrlog2bndlem1  21224  pntlem3  21256  umgrass  21307  umgran0  21308  umisuhgra  21315  usgrass  21337  usgrares1  21377  usgrafilem1  21378  nbgrassvt  21398  nbgraf1olem1  21404  cusgrares  21434  vdgrun  21625  vdgrfiun  21626  konigsberg  21662  ocsh  22738  spancl  22791  shsval2i  22842  ococin  22863  chsupid  22867  speccl  23355  atssch  23799  hatomistici  23818  chpssati  23819  iundisjf  23982  iundisjfi  24105  esumpinfval  24416  sigagensiga  24477  measvuni  24521  imambfm  24565  dya2iocuni  24586  ballotlemoex  24696  ballotlem2  24699  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemfmpn  24705  ballotlemiex  24712  ballotlemsup  24715  ballotlem7  24746  ballotth  24748  lgamucov  24775  lgamucov2  24776  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  erdszelem2  24831  conpcon  24875  cvmliftmolem2  24922  cvmliftlem15  24938  cvmlift2lem12  24954  snmlff  24969  tfisg  25418  wfisg  25423  frinsg  25459  sltval2  25524  nodenselem4  25552  nobndlem5  25564  nofulllem5  25574  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  axcontlem10  25816  rankeq1o  26016  mblfinlem  26143  ismblfin  26146  mbfposadd  26153  cnambfre  26154  finminlem  26211  fnessref  26263  finlocfin  26269  neibastop1  26278  neibastop2lem  26279  cover2  26305  indexa  26325  fdc  26339  sstotbnd2  26373  sstotbnd3  26375  igenidl  26563  prnc  26567  mzpindd  26693  fiphp3d  26770  rencldnfilem  26771  irrapx1  26781  pellexlem3  26784  pellfundre  26834  pellfundge  26835  pellfundlb  26837  pellfundglb  26838  jm2.22  26956  jm2.23  26957  rpnnen3  26993  fglmod  27039  pwssplit4  27059  dsmmbase  27069  dsmmval2  27070  dsmmsubg  27077  frlmsslsp  27116  pwfi2f1o  27128  hbtlem6  27201  dgraalem  27218  dgraaub  27221  itgocn  27237  rgspncl  27242  issubmd  27251  symgsssg  27276  symgfisg  27277  psgnghm  27305  phisum  27386  stoweidlem14  27630  stoweidlem34  27650  stoweidlem44  27660  stoweidlem50  27666  stoweidlem51  27667  stoweidlem52  27668  stoweidlem57  27673  stoweidlem59  27675  frisusgranb  28101  frgrawopreg1  28153  frgrawopreg2  28154  bnj21  28788  bnj110  28935  bnj1204  29087  bnj1311  29099  toycom  29455  lkrlss  29578  atlatmstc  29802  atlatle  29803  glbconN  29859  linepsubN  30234  pmapssat  30241  pmaple  30243  pmapsub  30250  paddssat  30296  diass  31525  diaglbN  31538  diaintclN  31541  diassdvaN  31543  docaclN  31607  dibglbN  31649  dibintclN  31650  diclspsn  31677  dihglblem2N  31777  dih1dimatlem  31812  dihglb2  31825  dochval2  31835  dochcl  31836  dochvalr  31840  doch2val2  31847  dochss  31848  dochocss  31849  lclkr  32016  lclkrs  32022  lcdvbase  32076  lcdvbasess  32077  mapdunirnN  32133
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator