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

Theorem ssrab2 3720
 Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
ssrab2 {𝑥𝐴𝜑} ⊆ 𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab2
StepHypRef Expression
1 df-rab 2950 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 3719 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3668 1 {𝑥𝐴𝜑} ⊆ 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   ∈ wcel 2030  {cab 2637  {crab 2945   ⊆ wss 3607 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-in 3614  df-ss 3621 This theorem is referenced by:  ssrab3  3721  ssrabeq  3722  iinrab2  4615  riinrab  4628  rabexg  4844  pwnss  4860  frminex  5123  wereu2  5140  dmmptss  5669  wfisg  5753  ssimaex  6302  f1oresrab  6435  weniso  6644  canth  6648  riotacl  6665  riotassuni  6688  onminesb  7040  onminsb  7041  onintrab  7043  onnminsb  7046  onminex  7049  tfis  7096  omsson  7111  suppssdm  7353  fnsuppres  7367  oawordeulem  7679  oeeulem  7726  nnawordex  7762  pmvalg  7910  fineqvlem  8215  ordtypelem2  8465  ordtypelem3  8466  ordtypelem4  8467  ordtypelem6  8469  hartogs  8490  wemapso2lem  8498  card2on  8500  wdom2d  8526  oemapvali  8619  wemapwe  8632  tz9.12lem1  8688  tz9.12lem3  8690  rankf  8695  cplem1  8790  cardf2  8807  cardid2  8817  cardmin2  8862  acni3  8908  dfac2a  8990  cofsmo  9129  coftr  9133  fin2i2  9178  isfin2-2  9179  enfin2i  9181  fin23lem28  9200  fin23lem30  9202  isf32lem5  9217  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  fin1a2lem11  9270  fin1a2lem12  9271  hsmexlem4  9289  hsmexlem5  9290  hsmexlem6  9291  axdc3lem4  9313  ac6num  9339  ac6  9340  zorn2lem1  9356  zorn2lem3  9358  zorn2lem4  9359  zorn2lem5  9360  ondomon  9423  alephval2  9432  pwfseqlem1  9518  pwfseqlem3  9520  wunccl  9604  tskmcl  9701  0nnq  9784  elpqn  9785  fiminre  11010  infm3  11020  uzf  11728  nnwos  11793  supminf  11813  zsupss  11815  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  rpre  11877  ixxf  12223  fzf  12368  flval3  12656  rabssnn0fi  12825  expge0  12936  expge1  12937  hashbclem  13274  sqrlem3  14029  sqrlem5  14031  rlimrege0  14354  incexc2  14614  dvdsflip  15086  divalglem2  15165  divalglem5  15167  divalglem8  15170  bitsf  15196  bitsfzolem  15203  sadadd2lem  15228  sadadd3  15230  sadcl  15231  smupf  15247  smuval2  15251  smupvallem  15252  smucl  15253  smueqlem  15259  gcdcllem3  15270  bezoutlem2  15304  bezoutlem3  15305  lcmcllem  15356  lcmn0cl  15357  lcmledvds  15359  lcmfval  15381  lcmfcllem  15385  lcmfn0cl  15386  lcmfledvds  15392  maxprmfct  15468  phicl2  15520  phibnd  15523  hashdvds  15527  phiprmpw  15528  phimullem  15531  eulerthlem2  15534  eulerth  15535  phisum  15542  odzcllem  15544  odzdvds  15547  pclem  15590  infpn2  15664  prmreclem1  15667  prmreclem2  15668  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  4sqlem13  15708  4sqlem14  15709  4sqlem17  15712  4sqlem18  15713  vdwnnlem3  15748  hashbccl  15754  ramcl2lem  15760  ramtcl  15761  ramtcl2  15762  ramtub  15763  prmgaplem3  15804  prmgaplem4  15805  prdsds  16171  imasdsval2  16223  mrcflem  16313  isacs1i  16365  wunnat  16663  dmcoass  16763  lublecl  17036  lubid  17037  gsumval1  17324  issubmd  17396  mhmeql  17411  nmzsubg  17682  nmznsg  17685  conjnmz  17741  conjnmzb  17742  gastacl  17788  cntzval  17800  cntzssv  17807  symgsssg  17933  symgfisg  17934  pmtrdifellem4  17945  odlem1  18000  odlem2  18004  odngen  18038  gexlem1  18040  gexlem2  18043  sylow1lem2  18060  sylow1lem3  18061  sylow1lem4  18062  sylow1lem5  18063  sylow2alem2  18079  sylow2a  18080  sylow2blem3  18083  sylow3lem2  18089  oddvdssubg  18304  cyggex2  18344  ablfacrplem  18510  ablfacrp2  18512  ablfac1eu  18518  pgpfaclem1  18526  ablfaclem2  18531  ablfaclem3  18532  lssacs  19015  lspf  19022  lspsolvlem  19190  lbsextlem2  19207  lbsextlem3  19208  lbsextlem4  19209  rrgeq0  19338  rrgss  19340  asplss  19377  aspsubrg  19379  psrbagconf1o  19422  psrass1lem  19425  psrdi  19454  psrdir  19455  psrass23l  19456  psrass23  19458  resspsrmul  19465  mplbas  19477  mplbasss  19480  mplsubglem  19482  mplsubrglem  19487  mplmonmul  19512  psropprmul  19656  coe1mul2lem2  19686  cygznlem2a  19964  psgnghm  19974  ocvfval  20058  ocvval  20059  dsmmbase  20127  dsmmval2  20128  dsmmsubg  20135  frlmsslsp  20183  scmatlss  20379  smadiadet  20524  pmatcoe1fsupp  20554  cpmatsubgpmat  20573  fctop  20856  cctop  20858  ppttop  20859  epttop  20861  clscld  20899  mretopd  20944  neips  20965  neiptopnei  20984  ordtbaslem  21040  ordtuni  21042  ordtcld1  21049  ordtcld2  21050  cnpfval  21086  iscnp2  21091  cmpcov2  21241  cmpsublem  21250  tgcmp  21252  hauscmplem  21257  conncompcld  21285  1stcfb  21296  2ndc1stc  21302  2ndcdisj  21307  finlocfin  21371  kgentopon  21389  xkotf  21436  txkgen  21503  xkococnlem  21510  imastopn  21571  kqffn  21576  opnfbas  21693  flimfnfcls  21879  alexsubALT  21902  ptcmplem1  21903  ptcmplem2  21904  ptcmplem3  21905  symgtgp  21952  tgpconncompeqg  21962  tgpconncomp  21963  ghmcnp  21965  tsmsfbas  21978  eltsms  21983  utoptop  22085  utopbas  22086  imasdsf1olem  22225  blfvalps  22235  blfps  22258  blf  22259  blcld  22357  nmoffn  22562  nmofval  22565  nmogelb  22567  nmolb  22568  nmof  22570  icccmplem1  22672  icccmplem2  22673  icccmplem3  22674  ishtpy  22818  clsocv  23095  rrxnm  23225  rrxf  23230  minveclem3b  23245  minveclem4  23249  ivthlem1  23266  ivthlem2  23267  ivthlem3  23268  ovolcl  23292  ovollb  23293  ovolgelb  23294  ovolge0  23295  ovolsslem  23298  ovolshftlem1  23323  ovolshft  23325  ovolscalem1  23327  ovolscalem2  23328  ovolsca  23329  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicc2  23336  shftmbl  23352  iundisj  23362  dyadmax  23412  dyadmbllem  23413  dyadmbl  23414  opnmbllem  23415  iblmbf  23579  mdegmullem  23883  uc1pval  23944  mon1pval  23946  elqaalem1  24119  elqaalem3  24121  aannenlem2  24129  aalioulem2  24133  radcnvcl  24216  radcnvlt1  24217  radcnvle  24219  abelthlem4  24233  abelthlem6  24235  abelthlem9  24239  abelth  24240  atancn  24708  lgamucov  24809  lgamucov2  24810  ftalem3  24846  ftalem4  24847  ftalem5  24848  efnnfsumcl  24874  isppw  24885  sgmval2  24914  efchtdvds  24930  sqff1o  24953  fsumdvdsdiaglem  24954  fsumdvdsdiag  24955  fsumdvdscom  24956  musum  24962  muinv  24964  dvdsmulf1o  24965  fsumdvdsmul  24966  sgmmul  24971  ppiub  24974  vmasum  24986  logfac2  24987  perfectlem2  25000  lgsfcl2  25073  lgsfcl  25075  lgscl  25081  lgsquadlem1  25150  lgsquadlem2  25151  rpvmasumlem  25221  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  dchrisum0  25254  mudivsum  25264  mulogsum  25266  mulog2sumlem2  25269  vmalogdivsum2  25272  logsqvma  25276  logsqvma2  25277  selberglem3  25281  selberg  25282  selberg34r  25305  pntsval2  25310  pntrlog2bndlem1  25311  pntlem3  25343  tglnunirn  25488  tglnssp  25492  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  axcontlem10  25898  incistruhgr  26019  upgrss  26028  upgrn0  26029  upgruhgr  26042  usgrss  26114  uspgrushgr  26115  ushgredgedg  26166  ushgredgedgloop  26168  upgrreslem  26241  umgrreslem  26242  vtxdun  26433  vtxdginducedm1lem2  26492  vtxdginducedm1  26495  finsumvtxdg2ssteplem1  26497  hashwwlksnext  26877  clwwlksswrd  26955  frcond3  27249  ocsh  28270  spancl  28323  shsval2i  28374  ococin  28395  chsupid  28399  speccl  28886  atssch  29330  hatomistici  29349  chpssati  29350  iundisjf  29528  aciunf1  29591  fcobijfs  29629  fpwrelmap  29636  iundisjfi  29683  locfinreflem  30035  esumrnmpt2  30258  esumpinfval  30263  sigagensiga  30332  ldgenpisyslem1  30354  ldgenpisys  30357  measvuni  30405  imambfm  30452  dya2iocuni  30473  omscl  30485  oms0  30487  omsmon  30488  omssubadd  30490  carsgcl  30494  oddpwdc  30544  eulerpartlem1  30557  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemmf  30565  eulerpartlemgh  30568  eulerpartlemgs2  30570  ballotlem2  30678  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemfmpn  30684  ballotlemiex  30691  ballotlemsup  30694  ballotlem7  30725  ballotth  30727  reprpmtf1o  30832  breprexplema  30836  hgt750lema  30863  bnj110  31054  bnj1204  31206  bnj1311  31218  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  erdszelem2  31300  connpconn  31343  cvmliftmolem2  31390  cvmliftlem15  31406  cvmlift2lem12  31422  snmlff  31437  tfisg  31840  frpomin  31863  frpoinsg  31866  frinsg  31870  wlimss  31899  sltval2  31934  conway  32035  scutun12  32042  scutbdaybnd  32046  scutbdaylt  32047  rankeq1o  32403  finminlem  32437  fnessref  32477  neibastop1  32479  neibastop2lem  32480  bj-rabtr  33051  bj-rabtrALTALT  33053  bj-rabtrAUTO  33054  bj-cmnssmnd  33266  bj-vecssmod  33273  bj-rrvecssvec  33280  icoreresf  33330  phpreu  33523  fin2so  33526  poimirlem26  33565  poimirlem31  33570  poimirlem32  33571  opnmbllem0  33575  mblfinlem1  33576  mblfinlem2  33577  ismblfin  33580  mbfposadd  33587  cnambfre  33588  cover2  33638  indexa  33658  fdc  33671  sstotbnd2  33703  sstotbnd3  33705  igenidl  33992  prnc  33996  toycom  34578  lkrlss  34700  atlatmstc  34924  atlatle  34925  glbconN  34981  linepsubN  35356  pmapssat  35363  pmaple  35365  pmapsub  35372  paddssat  35418  diass  36648  diaglbN  36661  diaintclN  36664  diassdvaN  36666  docaclN  36730  dibglbN  36772  dibintclN  36773  diclspsn  36800  dihglblem2N  36900  dih1dimatlem  36935  dihglb2  36948  dochval2  36958  dochcl  36959  dochvalr  36963  doch2val2  36970  dochss  36971  dochocss  36972  lclkr  37139  lclkrs  37145  lcdvbase  37199  lcdvbasess  37200  mapdunirnN  37256  mzpindd  37626  fiphp3d  37700  rencldnfilem  37701  irrapx1  37709  pellexlem3  37712  pellfundre  37762  pellfundge  37763  pellfundlb  37765  pellfundglb  37766  jm2.22  37879  jm2.23  37880  rpnnen3  37916  fglmod  37960  pwssplit4  37976  pwfi2f1o  37983  hbtlem6  38016  dgraalem  38032  dgraaub  38035  itgocn  38051  rgspncl  38056  rfovcnvf1od  38615  fsovfd  38623  fsovcnvlem  38624  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemnotnn0  38872  uzwo4  39535  disjf1o  39692  icof  39725  allbutfiinf  39960  supminfxr  40007  supminfxr2  40012  fsumsupp0  40128  limcperiod  40178  sumnnodd  40180  fnlimabslt  40229  liminfvalxr  40333  cncfshift  40405  cncfperiod  40410  ioodvbdlimc1lem1  40464  dvnprodlem1  40479  dvnprodlem2  40480  stoweidlem14  40549  stoweidlem34  40569  stoweidlem44  40579  stoweidlem50  40585  stoweidlem51  40586  stoweidlem52  40587  stoweidlem57  40592  stoweidlem59  40594  fourierdlem19  40661  fourierdlem20  40662  fourierdlem25  40667  fourierdlem31  40673  fourierdlem37  40679  fourierdlem42  40684  fourierdlem51  40692  fourierdlem54  40695  fourierdlem64  40705  fourierdlem79  40720  elaa2lem  40768  etransclem16  40785  etransclem24  40793  etransclem31  40800  etransclem33  40802  etransclem34  40803  etransclem48  40817  rrxbasefi  40821  salgencl  40868  salexct  40870  salgenuni  40873  subsaliuncllem  40893  meadjiunlem  41000  caragenss  41039  caratheodory  41063  ovnlecvr  41093  ovnsslelem  41095  ovnlerp  41097  ovn0lem  41100  ovnsubaddlem1  41105  hoidmv1lelem1  41126  hoidmv1lelem3  41128  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  ovnhoilem1  41136  ovnhoilem2  41137  ovnlecvr2  41145  ovncvr2  41146  opnvonmbllem2  41168  ovolval4lem1  41184  ovolval5lem3  41189  pimconstlt1  41236  pimltpnf  41237  pimiooltgt  41242  pimgtmnf2  41245  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  sssmf  41268  incsmflem  41271  smfaddlem1  41292  smfaddlem2  41293  decsmflem  41295  smflimlem1  41300  smflimlem2  41301  smflimlem3  41302  smfrec  41317  smfmullem4  41322  smfdiv  41325  smfsuplem1  41338  smfsuplem3  41340  smfinflem  41344  smflimsuplem1  41347  smflimsuplem7  41353  smfliminflem  41357  prmdvdsfmtnof1lem1  41821  prmdvdsfmtnof  41823  perfectALTVlem2  41956  sprsymrelfolem1  42067  rabsubmgmd  42116  mgmhmeql  42128  oddibas  42138  2zlidl  42259  2zrngbas  42261  2zrng0  42263
 Copyright terms: Public domain W3C validator