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

Theorem ssrab2 3430
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 2716 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3429 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3380 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360    e. wcel 1726   {cab 2424   {crab 2711    C_ wss 3322
This theorem is referenced by:  ssrabeq  3431  iinrab2  4156  riinrab  4169  rabexg  4356  pwnss  4368  frminex  4565  wereu2  4582  onminesb  4781  onminsb  4782  onintrab  4784  onnminsb  4787  onminex  4790  tfis  4837  omsson  4852  dmmptss  5369  ssimaex  5791  fnsuppres  5955  weniso  6078  canth  6542  riotacl  6567  riotassuni  6591  oawordeulem  6800  oeeulem  6847  nnawordex  6883  pmvalg  7032  fineqvlem  7326  ordtypelem2  7491  ordtypelem3  7492  ordtypelem4  7493  ordtypelem6  7495  hartogs  7516  wemapso2  7524  card2on  7525  wdom2d  7551  cantnfres  7636  oemapvali  7643  wemapwe  7657  tz9.12lem1  7716  tz9.12lem3  7718  rankf  7723  cplem1  7818  cardf2  7835  cardid2  7845  cardmin2  7890  acni3  7933  dfac2a  8015  cofsmo  8154  coftr  8158  fin2i2  8203  isfin2-2  8204  enfin2i  8206  fin23lem28  8225  fin23lem30  8227  isf32lem5  8242  isf32lem6  8243  isf32lem7  8244  isf32lem8  8245  fin1a2lem11  8295  fin1a2lem12  8296  hsmexlem4  8314  hsmexlem5  8315  hsmexlem6  8316  axdc3lem4  8338  ac6num  8364  ac6  8365  zorn2lem1  8381  zorn2lem3  8383  zorn2lem4  8384  zorn2lem5  8385  ondomon  8443  alephval2  8452  pwfseqlem1  8538  pwfseqlem3  8540  wunccl  8624  tskmcl  8721  0nnq  8806  elpqn  8807  infm3  9972  infmrcl  9992  uzf  10496  nnwos  10549  supminf  10568  zsupss  10570  rpnnen1lem1  10605  rpnnen1lem2  10606  rpnnen1lem3  10607  rpnnen1lem5  10609  rpre  10623  ixxf  10931  fzf  11052  flval3  11227  expge0  11421  expge1  11422  hashbclem  11706  sqrlem3  12055  sqrlem5  12057  rlimrege0  12378  incexc2  12623  divalglem2  12920  divalglem5  12922  divalglem8  12925  bitsf  12944  bitsfzolem  12951  sadadd2lem  12976  sadadd3  12978  sadcl  12979  smupf  12995  smuval2  12999  smupvallem  13000  smucl  13001  smueqlem  13007  gcdcllem3  13018  bezoutlem2  13044  bezoutlem3  13045  maxprmfct  13118  phicl2  13162  phibnd  13165  hashdvds  13169  phiprmpw  13170  phimullem  13173  eulerthlem2  13176  eulerth  13177  odzcllem  13183  odzdvds  13186  pclem  13217  infpn2  13286  prmreclem1  13289  prmreclem2  13290  prmreclem3  13291  prmreclem4  13292  prmreclem5  13293  4sqlem13  13330  4sqlem14  13331  4sqlem17  13334  4sqlem18  13335  vdwnnlem3  13370  hashbccl  13376  ramcl2lem  13382  ramtcl  13383  ramtcl2  13384  ramtub  13385  prdsds  13691  imasdsval2  13747  mrcflem  13836  isacs1i  13887  wunnat  14158  dmcoass  14226  lubid  14444  mhmeql  14769  gsumval1  14784  nmzsubg  14986  nmznsg  14989  conjnmz  15044  conjnmzb  15045  gastacl  15091  cntzval  15125  cntzssv  15132  odlem1  15178  odlem2  15182  odngen  15216  gexlem1  15218  gexlem2  15221  sylow1lem2  15238  sylow1lem3  15239  sylow1lem4  15240  sylow1lem5  15241  sylow2alem2  15257  sylow2a  15258  sylow2blem3  15261  sylow3lem2  15267  oddvdssubg  15475  cyggex2  15511  ablfacrplem  15628  ablfacrp2  15630  ablfac1eu  15636  pgpfaclem1  15644  ablfaclem2  15649  ablfaclem3  15650  lssacs  16048  lspf  16055  lspsolvlem  16219  lbsextlem2  16236  lbsextlem3  16237  lbsextlem4  16238  rrgeq0  16355  rrgss  16357  asplss  16393  aspsubrg  16395  psrbagconf1o  16444  psrass1lem  16447  psrdi  16475  psrdir  16476  psrass23  16478  resspsrmul  16485  mplbas  16498  mplbasss  16501  mplsubglem  16503  mplsubrglem  16507  mplmonmul  16532  psropprmul  16637  coe1mul2lem2  16666  cygznlem2a  16853  ocvfval  16898  ocvval  16899  fctop  17073  cctop  17075  ppttop  17076  epttop  17078  clscld  17116  mretopd  17161  neips  17182  neiptopnei  17201  ordtbaslem  17257  ordtuni  17259  ordtcld1  17266  ordtcld2  17267  cnpfval  17303  iscnp2  17308  cmpcov2  17458  cmpsublem  17467  tgcmp  17469  hauscmplem  17474  concompcld  17502  1stcfb  17513  2ndc1stc  17519  2ndcdisj  17524  kgentopon  17575  xkotf  17622  txkgen  17689  xkococnlem  17696  imastopn  17757  kqffn  17762  opnfbas  17879  flimfnfcls  18065  alexsubALT  18087  ptcmplem1  18088  ptcmplem2  18089  ptcmplem3  18090  symgtgp  18136  tgpconcompeqg  18146  tgpconcomp  18147  ghmcnp  18149  tsmsfbas  18162  eltsms  18167  utoptop  18269  utopbas  18270  imasdsf1olem  18408  blfvalps  18418  blfps  18441  blf  18442  blcld  18540  nmoffn  18750  nmofval  18753  nmogelb  18755  nmolb  18756  nmof  18758  icccmplem1  18858  icccmplem2  18859  icccmplem3  18860  ishtpy  19002  clsocv  19209  minveclem3b  19334  minveclem4  19338  ivthlem1  19353  ivthlem2  19354  ivthlem3  19355  ovolcl  19379  ovollb  19380  ovolgelb  19381  ovolge0  19382  ovolsslem  19385  ovolshftlem1  19410  ovolshft  19412  ovolscalem1  19414  ovolscalem2  19415  ovolsca  19416  ovolicc2lem3  19420  ovolicc2lem4  19421  ovolicc2lem5  19422  ovolicc2  19423  shftmbl  19438  iundisj  19447  dyadmax  19495  dyadmbllem  19496  dyadmbl  19497  opnmbllem  19498  iblmbf  19662  mdegmullem  20006  uc1pval  20067  mon1pval  20069  elqaalem1  20241  elqaalem3  20243  aannenlem2  20251  aalioulem2  20255  radcnvcl  20338  radcnvlt1  20339  radcnvle  20341  abelthlem4  20355  abelthlem6  20357  abelthlem9  20361  abelth  20362  atancn  20781  ftalem3  20862  ftalem4  20863  ftalem5  20864  efnnfsumcl  20890  isppw  20902  sgmval2  20931  efchtdvds  20947  sqff1o  20970  dvdsflip  20972  fsumdvdsdiaglem  20973  fsumdvdsdiag  20974  fsumdvdscom  20975  musum  20981  muinv  20983  dvdsmulf1o  20984  fsumdvdsmul  20985  sgmmul  20990  ppiub  20993  vmasum  21005  logfac2  21006  perfectlem2  21019  lgsfcl2  21091  lgsfcl  21093  lgscl  21099  lgseisenlem3  21140  lgseisenlem4  21141  lgsquadlem1  21143  lgsquadlem2  21144  rpvmasumlem  21186  rpvmasum2  21211  dchrisum0re  21212  dchrisum0lema  21213  dchrisum0lem1b  21214  dchrisum0lem1  21215  dchrisum0lem2a  21216  dchrisum0lem2  21217  dchrisum0lem3  21218  dchrisum0  21219  mudivsum  21229  mulogsum  21231  mulog2sumlem2  21234  vmalogdivsum2  21237  logsqvma  21241  logsqvma2  21242  selberglem3  21246  selberg  21247  selberg34r  21270  pntsval2  21275  pntrlog2bndlem1  21276  pntlem3  21308  umgrass  21359  umgran0  21360  umisuhgra  21367  usgrass  21389  usgrares1  21429  usgrafilem1  21430  nbgrassvt  21450  nbgraf1olem1  21456  cusgrares  21486  vdgrun  21677  vdgrfiun  21678  konigsberg  21714  ocsh  22790  spancl  22843  shsval2i  22894  ococin  22915  chsupid  22919  speccl  23407  atssch  23851  hatomistici  23870  chpssati  23871  iundisjf  24034  iundisjfi  24157  esumpinfval  24468  sigagensiga  24529  measvuni  24573  imambfm  24617  dya2iocuni  24638  ballotlemoex  24748  ballotlem2  24751  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemfmpn  24757  ballotlemiex  24764  ballotlemsup  24767  ballotlem7  24798  ballotth  24800  lgamucov  24827  lgamucov2  24828  subfacp1lem3  24873  subfacp1lem5  24875  subfacp1lem6  24876  erdszelem2  24883  conpcon  24927  cvmliftmolem2  24974  cvmliftlem15  24990  cvmlift2lem12  25006  snmlff  25021  tfisg  25484  wfisg  25489  frinsg  25525  wlimss  25585  sltval2  25616  nodenselem4  25644  nobndlem5  25656  nofulllem5  25666  axcontlem2  25909  axcontlem7  25914  axcontlem8  25915  axcontlem10  25917  rankeq1o  26117  opnmbllem0  26254  mblfinlem1  26255  mblfinlem2  26256  ismblfin  26259  mbfposadd  26266  cnambfre  26267  finminlem  26335  fnessref  26387  finlocfin  26393  neibastop1  26402  neibastop2lem  26403  cover2  26429  indexa  26449  fdc  26463  sstotbnd2  26497  sstotbnd3  26499  igenidl  26687  prnc  26691  mzpindd  26817  fiphp3d  26894  rencldnfilem  26895  irrapx1  26905  pellexlem3  26908  pellfundre  26958  pellfundge  26959  pellfundlb  26961  pellfundglb  26962  jm2.22  27080  jm2.23  27081  rpnnen3  27117  fglmod  27162  pwssplit4  27182  dsmmbase  27192  dsmmval2  27193  dsmmsubg  27200  frlmsslsp  27239  pwfi2f1o  27251  hbtlem6  27324  dgraalem  27341  dgraaub  27344  itgocn  27360  rgspncl  27365  issubmd  27374  symgsssg  27399  symgfisg  27400  psgnghm  27428  phisum  27509  stoweidlem14  27753  stoweidlem34  27773  stoweidlem44  27783  stoweidlem50  27789  stoweidlem51  27790  stoweidlem52  27791  stoweidlem57  27796  stoweidlem59  27798  frisusgranb  28461  frgrawopreg1  28513  frgrawopreg2  28514  bnj21  29156  bnj110  29303  bnj1204  29455  bnj1311  29467  toycom  29844  lkrlss  29967  atlatmstc  30191  atlatle  30192  glbconN  30248  linepsubN  30623  pmapssat  30630  pmaple  30632  pmapsub  30639  paddssat  30685  diass  31914  diaglbN  31927  diaintclN  31930  diassdvaN  31932  docaclN  31996  dibglbN  32038  dibintclN  32039  diclspsn  32066  dihglblem2N  32166  dih1dimatlem  32201  dihglb2  32214  dochval2  32224  dochcl  32225  dochvalr  32229  doch2val2  32236  dochss  32237  dochocss  32238  lclkr  32405  lclkrs  32411  lcdvbase  32465  lcdvbasess  32466  mapdunirnN  32522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator