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

Theorem ssrab2 3552
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 2791 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3551 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3500 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    e. wcel 1870   {cab 2414   {crab 2786    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-in 3449  df-ss 3456
This theorem is referenced by:  ssrabeq  3553  iinrab2  4365  riinrab  4378  rabexg  4575  pwnss  4590  frminex  4834  wereu2  4851  dmmptss  5351  wfisg  5434  ssimaex  5946  f1oresrab  6070  weniso  6260  canth  6264  riotacl  6281  riotassuni  6303  onminesb  6639  onminsb  6640  onintrab  6642  onnminsb  6645  onminex  6648  tfis  6695  omsson  6710  suppssdm  6938  fnsuppres  6953  oawordeulem  7263  oeeulem  7310  nnawordex  7346  pmvalg  7491  fineqvlem  7792  ordtypelem2  8034  ordtypelem3  8035  ordtypelem4  8036  ordtypelem6  8038  hartogs  8059  wemapso2lem  8067  card2on  8069  wdom2d  8095  oemapvali  8188  wemapwe  8201  tz9.12lem1  8257  tz9.12lem3  8259  rankf  8264  cplem1  8359  cardf2  8376  cardid2  8386  cardmin2  8431  acni3  8476  dfac2a  8558  cofsmo  8697  coftr  8701  fin2i2  8746  isfin2-2  8747  enfin2i  8749  fin23lem28  8768  fin23lem30  8770  isf32lem5  8785  isf32lem6  8786  isf32lem7  8787  isf32lem8  8788  fin1a2lem11  8838  fin1a2lem12  8839  hsmexlem4  8857  hsmexlem5  8858  hsmexlem6  8859  axdc3lem4  8881  ac6num  8907  ac6  8908  zorn2lem1  8924  zorn2lem3  8926  zorn2lem4  8927  zorn2lem5  8928  ondomon  8986  alephval2  8995  pwfseqlem1  9082  pwfseqlem3  9084  wunccl  9168  tskmcl  9265  0nnq  9348  elpqn  9349  fiminre  10555  infm3  10568  infmrclOLD  10593  uzf  11162  nnwos  11226  supminf  11250  supminfOLD  11251  zsupss  11253  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  rpre  11308  ixxf  11645  fzf  11786  flval3  12047  rabssnn0fi  12195  expge0  12305  expge1  12306  hashbclem  12610  sqrlem3  13287  sqrlem5  13289  rlimrege0  13621  incexc2  13874  divalglem2  14351  divalglem5  14353  divalglem8  14356  bitsf  14375  bitsfzolem  14382  sadadd2lem  14407  sadadd3  14409  sadcl  14410  smupf  14426  smuval2  14430  smupvallem  14431  smucl  14432  smueqlem  14438  gcdcllem3  14449  bezoutlem2  14478  bezoutlem3  14479  lcmcllem  14532  lcmn0cl  14533  lcmledvds  14535  lcmscllemOLD  14553  lcmsnnOLD  14554  lcmsledvdsOLD  14556  lcmfval  14562  lcmfvalOLD  14566  lcmfcllem  14569  lcmfn0cl  14570  lcmfledvds  14576  maxprmfct  14623  phicl2  14685  phibnd  14688  hashdvds  14692  phiprmpw  14693  phimullem  14696  eulerthlem2  14699  eulerth  14700  odzcllem  14706  odzdvds  14709  pclem  14751  infpn2  14820  prmreclem1  14823  prmreclem2  14824  prmreclem3  14825  prmreclem4  14826  prmreclem5  14827  4sqlem13OLD  14864  4sqlem14OLD  14865  4sqlem17OLD  14868  4sqlem18OLD  14869  4sqlem13  14870  4sqlem14  14871  4sqlem17  14874  4sqlem18  14875  vdwnnlem3  14910  hashbccl  14918  ramcl2lem  14925  ramcl2lemOLD  14926  ramtcl  14927  ramtclOLD  14928  ramtcl2  14929  ramtcl2OLD  14930  ramtub  14931  ramtubOLD  14932  prmordvdslcmsOLDOLD  14984  prmgaplem3  14986  prmgaplem4  14987  prdsds  15321  imasdsval2  15373  mrcflem  15463  isacs1i  15514  wunnat  15812  dmcoass  15912  lublecl  16186  lubid  16187  gsumval1  16471  issubmd  16547  mhmeql  16562  nmzsubg  16809  nmznsg  16812  conjnmz  16867  conjnmzb  16868  gastacl  16914  cntzval  16926  cntzssv  16933  symgsssg  17059  symgfisg  17060  pmtrdifellem4  17071  odlem1  17126  odlem2  17130  odngen  17164  gexlem1  17166  gexlem2  17169  sylow1lem2  17186  sylow1lem3  17187  sylow1lem4  17188  sylow1lem5  17189  sylow2alem2  17205  sylow2a  17206  sylow2blem3  17209  sylow3lem2  17215  oddvdssubg  17428  cyggex2  17466  ablfacrplem  17633  ablfacrp2  17635  ablfac1eu  17641  pgpfaclem1  17649  ablfaclem2  17654  ablfaclem3  17655  lssacs  18125  lspf  18132  lspsolvlem  18300  lbsextlem2  18317  lbsextlem3  18318  lbsextlem4  18319  rrgeq0  18449  rrgss  18451  asplss  18488  aspsubrg  18490  psrbagconf1o  18533  psrass1lem  18536  psrdi  18565  psrdir  18566  psrass23l  18567  psrass23  18569  resspsrmul  18576  mplbas  18588  mplbasss  18591  mplsubglem  18593  mplsubrglem  18598  mplmonmul  18623  psropprmul  18766  coe1mul2lem2  18796  cygznlem2a  19069  psgnghm  19079  ocvfval  19160  ocvval  19161  dsmmbase  19229  dsmmval2  19230  dsmmsubg  19237  frlmsslsp  19285  scmatlss  19481  smadiadet  19626  pmatcoe1fsupp  19656  cpmatsubgpmat  19675  fctop  19950  cctop  19952  ppttop  19953  epttop  19955  clscld  19993  mretopd  20039  neips  20060  neiptopnei  20079  ordtbaslem  20135  ordtuni  20137  ordtcld1  20144  ordtcld2  20145  cnpfval  20181  iscnp2  20186  cmpcov2  20336  cmpsublem  20345  tgcmp  20347  hauscmplem  20352  concompcld  20380  1stcfb  20391  2ndc1stc  20397  2ndcdisj  20402  finlocfin  20466  kgentopon  20484  xkotf  20531  txkgen  20598  xkococnlem  20605  imastopn  20666  kqffn  20671  opnfbas  20788  flimfnfcls  20974  alexsubALT  20997  ptcmplem1  20998  ptcmplem2  20999  ptcmplem3  21000  symgtgp  21047  tgpconcompeqg  21057  tgpconcomp  21058  ghmcnp  21060  tsmsfbas  21073  eltsms  21078  utoptop  21180  utopbas  21181  imasdsf1olem  21319  blfvalps  21329  blfps  21352  blf  21353  blcld  21451  nmoffn  21643  nmofval  21646  nmogelb  21648  nmolb  21649  nmof  21651  icccmplem1  21751  icccmplem2  21752  icccmplem3  21753  ishtpy  21896  clsocv  22114  rrxnm  22243  rrxf  22248  minveclem3b  22263  minveclem4  22267  ivthlem1  22283  ivthlem2  22284  ivthlem3  22285  ovolcl  22309  ovollb  22310  ovolgelb  22311  ovolge0  22312  ovolsslem  22315  ovolshftlem1  22340  ovolshft  22342  ovolscalem1  22344  ovolscalem2  22345  ovolsca  22346  ovolicc2lem3  22350  ovolicc2lem4  22351  ovolicc2lem5  22352  ovolicc2  22353  shftmbl  22369  iundisj  22378  dyadmax  22433  dyadmbllem  22434  dyadmbl  22435  opnmbllem  22436  iblmbf  22602  mdegmullem  22904  uc1pval  22965  mon1pval  22967  elqaalem1  23140  elqaalem3  23142  aannenlem2  23150  aalioulem2  23154  radcnvcl  23237  radcnvlt1  23238  radcnvle  23240  abelthlem4  23254  abelthlem6  23256  abelthlem9  23260  abelth  23261  atancn  23727  lgamucov  23828  lgamucov2  23829  ftalem3  23864  ftalem4  23865  ftalem5  23866  efnnfsumcl  23892  isppw  23904  sgmval2  23933  efchtdvds  23949  sqff1o  23972  dvdsflip  23974  fsumdvdsdiaglem  23975  fsumdvdsdiag  23976  fsumdvdscom  23977  musum  23983  muinv  23985  dvdsmulf1o  23986  fsumdvdsmul  23987  sgmmul  23992  ppiub  23995  vmasum  24007  logfac2  24008  perfectlem2  24021  lgsfcl2  24093  lgsfcl  24095  lgscl  24101  lgsquadlem1  24145  lgsquadlem2  24146  rpvmasumlem  24188  rpvmasum2  24213  dchrisum0re  24214  dchrisum0lema  24215  dchrisum0lem1b  24216  dchrisum0lem1  24217  dchrisum0lem2a  24218  dchrisum0lem2  24219  dchrisum0lem3  24220  dchrisum0  24221  mudivsum  24231  mulogsum  24233  mulog2sumlem2  24236  vmalogdivsum2  24239  logsqvma  24243  logsqvma2  24244  selberglem3  24248  selberg  24249  selberg34r  24272  pntsval2  24277  pntrlog2bndlem1  24278  pntlem3  24310  tglnunirn  24453  tglnssp  24457  axcontlem2  24841  axcontlem7  24846  axcontlem8  24847  axcontlem10  24849  umgrass  24892  umgran0  24893  umisuhgra  24900  usgrass  24934  uslisushgra  24936  usgrares1  24983  usgrafilem1  24984  nbgrassvt  25006  nbgraf1olem1  25014  cusgrares  25045  hashwwlkext  25319  clwwlksswrd  25350  vdgrun  25474  vdgrfiun  25475  konigsberg  25560  frisusgranb  25570  frgrawopreg1  25623  frgrawopreg2  25624  ocsh  26771  spancl  26824  shsval2i  26875  ococin  26896  chsupid  26900  speccl  27387  atssch  27831  hatomistici  27850  chpssati  27851  iundisjf  28038  aciunf1  28105  fcobijfs  28154  fpwrelmap  28161  iundisjfi  28208  locfinreflem  28506  esumrnmpt2  28728  esumpinfval  28733  sigagensiga  28802  ldgenpisyslem1  28824  ldgenpisys  28827  measvuni  28875  imambfm  28923  dya2iocuni  28944  omscl  28956  oms0  28958  omsmon  28959  omssubadd  28961  carsgcl  28965  oddpwdc  29013  eulerpartlem1  29026  eulerpartlemt  29030  eulerpartgbij  29031  eulerpartlemmf  29034  eulerpartlemgvv  29035  eulerpartlemgh  29037  eulerpartlemgs2  29039  ballotlem2  29147  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemfmpn  29153  ballotlemiex  29160  ballotlemsup  29163  ballotlem7  29194  ballotth  29196  bnj21  29311  bnj110  29457  bnj1204  29609  bnj1311  29621  subfacp1lem3  29693  subfacp1lem5  29695  subfacp1lem6  29696  erdszelem2  29703  conpcon  29746  cvmliftmolem2  29793  cvmliftlem15  29809  cvmlift2lem12  29825  snmlff  29840  tfisg  30244  frinsg  30270  wlimss  30299  sltval2  30330  nodenselem4  30358  nobndlem5  30370  nofulllem5  30380  rankeq1o  30723  finminlem  30759  fnessref  30798  neibastop1  30800  neibastop2lem  30801  bj-rabtr  31283  bj-rabtrAUTO  31285  bj-cmnssmnd  31436  bj-vecssmod  31443  bj-rrvecssvec  31450  icoreresf  31489  phpreu  31633  fin2so  31636  poimirlem26  31670  poimirlem31  31675  poimirlem32  31676  opnmbllem0  31680  mblfinlem1  31681  mblfinlem2  31682  ismblfin  31685  mbfposadd  31692  cnambfre  31693  cover2  31744  indexa  31764  fdc  31778  sstotbnd2  31810  sstotbnd3  31812  igenidl  32000  prnc  32004  toycom  32248  lkrlss  32370  atlatmstc  32594  atlatle  32595  glbconN  32651  linepsubN  33026  pmapssat  33033  pmaple  33035  pmapsub  33042  paddssat  33088  diass  34319  diaglbN  34332  diaintclN  34335  diassdvaN  34337  docaclN  34401  dibglbN  34443  dibintclN  34444  diclspsn  34471  dihglblem2N  34571  dih1dimatlem  34606  dihglb2  34619  dochval2  34629  dochcl  34630  dochvalr  34634  doch2val2  34641  dochss  34642  dochocss  34643  lclkr  34810  lclkrs  34816  lcdvbase  34870  lcdvbasess  34871  mapdunirnN  34927  mzpindd  35297  fiphp3d  35371  rencldnfilem  35372  irrapx1  35382  pellexlem3  35385  pellfundre  35435  pellfundge  35436  pellfundlb  35438  pellfundglb  35439  jm2.22  35556  jm2.23  35557  rpnnen3  35593  fglmod  35637  pwssplit4  35653  pwfi2f1o  35660  hbtlem6  35694  dgraalem  35710  dgraaub  35713  itgocn  35729  rgspncl  35734  phisum  35775  binomcxplemdvbinom  36339  binomcxplemcvg  36340  binomcxplemnotnn0  36342  uzwo4  37033  disjf1o  37089  limcperiod  37280  sumnnodd  37282  cncfshift  37323  cncfperiod  37328  ioodvbdlimc1lem1  37375  dvnprodlem1  37390  dvnprodlem2  37391  stoweidlem14  37443  stoweidlem34  37464  stoweidlem44  37474  stoweidlem50  37480  stoweidlem51  37481  stoweidlem52  37482  stoweidlem57  37487  stoweidlem59  37489  fourierdlem19  37557  fourierdlem20  37558  fourierdlem25  37563  fourierdlem31  37569  fourierdlem37  37575  fourierdlem42  37580  fourierdlem51  37589  fourierdlem54  37592  fourierdlem64  37602  fourierdlem79  37617  elaa2lem  37665  etransclem16  37682  etransclem24  37690  etransclem31  37697  etransclem33  37699  etransclem34  37700  etransclem48  37714  salgencl  37737  meadjiunlem  37812  caragenss  37834  caratheodory  37858  perfectALTVlem2  38234  rabsubmgmd  38549  mgmhmeql  38561  oddibas  38571  2zlidl  38692  2zrngbas  38694  2zrng0  38696
  Copyright terms: Public domain W3C validator