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

Theorem ssrab2 3649
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 2904 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 3648 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3597 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 1976  {cab 2595  {crab 2899  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-in 3546  df-ss 3553
This theorem is referenced by:  ssrabeq  3650  iinrab2  4513  riinrab  4526  rabexg  4733  pwnss  4750  frminex  5007  wereu2  5024  dmmptss  5533  wfisg  5617  ssimaex  6157  f1oresrab  6286  weniso  6481  canth  6485  riotacl  6502  riotassuni  6524  onminesb  6867  onminsb  6868  onintrab  6870  onnminsb  6873  onminex  6876  tfis  6923  omsson  6938  suppssdm  7172  fnsuppres  7186  oawordeulem  7498  oeeulem  7545  nnawordex  7581  pmvalg  7732  fineqvlem  8036  ordtypelem2  8284  ordtypelem3  8285  ordtypelem4  8286  ordtypelem6  8288  hartogs  8309  wemapso2lem  8317  card2on  8319  wdom2d  8345  oemapvali  8441  wemapwe  8454  tz9.12lem1  8510  tz9.12lem3  8512  rankf  8517  cplem1  8612  cardf2  8629  cardid2  8639  cardmin2  8684  acni3  8730  dfac2a  8812  cofsmo  8951  coftr  8955  fin2i2  9000  isfin2-2  9001  enfin2i  9003  fin23lem28  9022  fin23lem30  9024  isf32lem5  9039  isf32lem6  9040  isf32lem7  9041  isf32lem8  9042  fin1a2lem11  9092  fin1a2lem12  9093  hsmexlem4  9111  hsmexlem5  9112  hsmexlem6  9113  axdc3lem4  9135  ac6num  9161  ac6  9162  zorn2lem1  9178  zorn2lem3  9180  zorn2lem4  9181  zorn2lem5  9182  ondomon  9241  alephval2  9250  pwfseqlem1  9336  pwfseqlem3  9338  wunccl  9422  tskmcl  9519  0nnq  9602  elpqn  9603  fiminre  10823  infm3  10833  uzf  11524  nnwos  11589  supminf  11609  zsupss  11611  rpnnen1lem2  11648  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  rpre  11673  ixxf  12014  fzf  12158  flval3  12435  rabssnn0fi  12604  expge0  12715  expge1  12716  hashbclem  13047  sqrlem3  13781  sqrlem5  13783  rlimrege0  14106  incexc2  14357  dvdsflip  14825  divalglem2  14904  divalglem5  14906  divalglem8  14909  bitsf  14935  bitsfzolem  14942  sadadd2lem  14967  sadadd3  14969  sadcl  14970  smupf  14986  smuval2  14990  smupvallem  14991  smucl  14992  smueqlem  14998  gcdcllem3  15009  bezoutlem2  15043  bezoutlem3  15044  lcmcllem  15095  lcmn0cl  15096  lcmledvds  15098  lcmfval  15120  lcmfcllem  15124  lcmfn0cl  15125  lcmfledvds  15131  maxprmfct  15207  phicl2  15259  phibnd  15262  hashdvds  15266  phiprmpw  15267  phimullem  15270  eulerthlem2  15273  eulerth  15274  phisum  15281  odzcllem  15283  odzdvds  15286  pclem  15329  infpn2  15403  prmreclem1  15406  prmreclem2  15407  prmreclem3  15408  prmreclem4  15409  prmreclem5  15410  4sqlem13  15447  4sqlem14  15448  4sqlem17  15451  4sqlem18  15452  vdwnnlem3  15487  hashbccl  15493  ramcl2lem  15499  ramtcl  15500  ramtcl2  15501  ramtub  15502  prmgaplem3  15543  prmgaplem4  15544  prdsds  15895  imasdsval2  15947  mrcflem  16037  isacs1i  16089  wunnat  16387  dmcoass  16487  lublecl  16760  lubid  16761  gsumval1  17048  issubmd  17120  mhmeql  17135  nmzsubg  17406  nmznsg  17409  conjnmz  17465  conjnmzb  17466  gastacl  17513  cntzval  17525  cntzssv  17532  symgsssg  17658  symgfisg  17659  pmtrdifellem4  17670  odlem1  17725  odlem2  17729  odngen  17763  gexlem1  17765  gexlem2  17768  sylow1lem2  17785  sylow1lem3  17786  sylow1lem4  17787  sylow1lem5  17788  sylow2alem2  17804  sylow2a  17805  sylow2blem3  17808  sylow3lem2  17814  oddvdssubg  18029  cyggex2  18069  ablfacrplem  18235  ablfacrp2  18237  ablfac1eu  18243  pgpfaclem1  18251  ablfaclem2  18256  ablfaclem3  18257  lssacs  18736  lspf  18743  lspsolvlem  18911  lbsextlem2  18928  lbsextlem3  18929  lbsextlem4  18930  rrgeq0  19059  rrgss  19061  asplss  19098  aspsubrg  19100  psrbagconf1o  19143  psrass1lem  19146  psrdi  19175  psrdir  19176  psrass23l  19177  psrass23  19179  resspsrmul  19186  mplbas  19198  mplbasss  19201  mplsubglem  19203  mplsubrglem  19208  mplmonmul  19233  psropprmul  19377  coe1mul2lem2  19407  cygznlem2a  19682  psgnghm  19692  ocvfval  19776  ocvval  19777  dsmmbase  19845  dsmmval2  19846  dsmmsubg  19853  frlmsslsp  19901  scmatlss  20097  smadiadet  20242  pmatcoe1fsupp  20272  cpmatsubgpmat  20291  fctop  20565  cctop  20567  ppttop  20568  epttop  20570  clscld  20608  mretopd  20653  neips  20674  neiptopnei  20693  ordtbaslem  20749  ordtuni  20751  ordtcld1  20758  ordtcld2  20759  cnpfval  20795  iscnp2  20800  cmpcov2  20950  cmpsublem  20959  tgcmp  20961  hauscmplem  20966  concompcld  20994  1stcfb  21005  2ndc1stc  21011  2ndcdisj  21016  finlocfin  21080  kgentopon  21098  xkotf  21145  txkgen  21212  xkococnlem  21219  imastopn  21280  kqffn  21285  opnfbas  21403  flimfnfcls  21589  alexsubALT  21612  ptcmplem1  21613  ptcmplem2  21614  ptcmplem3  21615  symgtgp  21662  tgpconcompeqg  21672  tgpconcomp  21673  ghmcnp  21675  tsmsfbas  21688  eltsms  21693  utoptop  21795  utopbas  21796  imasdsf1olem  21935  blfvalps  21945  blfps  21968  blf  21969  blcld  22067  nmoffn  22272  nmofval  22275  nmogelb  22277  nmolb  22278  nmof  22280  icccmplem1  22380  icccmplem2  22381  icccmplem3  22382  ishtpy  22526  clsocv  22801  rrxnm  22931  rrxf  22936  minveclem3b  22951  minveclem4  22955  ivthlem1  22971  ivthlem2  22972  ivthlem3  22973  ovolcl  22997  ovollb  22998  ovolgelb  22999  ovolge0  23000  ovolsslem  23003  ovolshftlem1  23028  ovolshft  23030  ovolscalem1  23032  ovolscalem2  23033  ovolsca  23034  ovolicc2lem3  23038  ovolicc2lem4  23039  ovolicc2lem5  23040  ovolicc2  23041  shftmbl  23057  iundisj  23067  dyadmax  23116  dyadmbllem  23117  dyadmbl  23118  opnmbllem  23119  iblmbf  23284  mdegmullem  23586  uc1pval  23647  mon1pval  23649  elqaalem1  23822  elqaalem3  23824  aannenlem2  23832  aalioulem2  23836  radcnvcl  23919  radcnvlt1  23920  radcnvle  23922  abelthlem4  23936  abelthlem6  23938  abelthlem9  23942  abelth  23943  atancn  24407  lgamucov  24508  lgamucov2  24509  ftalem3  24545  ftalem4  24546  ftalem5  24547  efnnfsumcl  24573  isppw  24584  sgmval2  24613  efchtdvds  24629  sqff1o  24652  fsumdvdsdiaglem  24653  fsumdvdsdiag  24654  fsumdvdscom  24655  musum  24661  muinv  24663  dvdsmulf1o  24664  fsumdvdsmul  24665  sgmmul  24670  ppiub  24673  vmasum  24685  logfac2  24686  perfectlem2  24699  lgsfcl2  24772  lgsfcl  24774  lgscl  24780  lgsquadlem1  24849  lgsquadlem2  24850  rpvmasumlem  24920  rpvmasum2  24945  dchrisum0re  24946  dchrisum0lema  24947  dchrisum0lem1b  24948  dchrisum0lem1  24949  dchrisum0lem2a  24950  dchrisum0lem2  24951  dchrisum0lem3  24952  dchrisum0  24953  mudivsum  24963  mulogsum  24965  mulog2sumlem2  24968  vmalogdivsum2  24971  logsqvma  24975  logsqvma2  24976  selberglem3  24980  selberg  24981  selberg34r  25004  pntsval2  25009  pntrlog2bndlem1  25010  pntlem3  25042  tglnunirn  25188  tglnssp  25192  axcontlem2  25590  axcontlem7  25595  axcontlem8  25596  axcontlem10  25598  umgrass  25641  umgran0  25642  umisuhgra  25649  usgrass  25683  uslisushgra  25685  usgrares1  25732  usgrafilem1  25733  nbgrassvt  25755  nbgraf1olem1  25763  cusgrares  25794  hashwwlkext  26067  clwwlksswrd  26098  vdgrun  26221  vdgrfiun  26222  konigsberg  26307  frisusgranb  26317  frgrawopreg1  26370  frgrawopreg2  26371  ocsh  27319  spancl  27372  shsval2i  27423  ococin  27444  chsupid  27448  speccl  27935  atssch  28379  hatomistici  28398  chpssati  28399  iundisjf  28577  aciunf1  28638  fcobijfs  28682  fpwrelmap  28689  iundisjfi  28735  locfinreflem  29028  esumrnmpt2  29250  esumpinfval  29255  sigagensiga  29324  ldgenpisyslem1  29346  ldgenpisys  29349  measvuni  29397  imambfm  29444  dya2iocuni  29465  omscl  29477  oms0  29479  omsmon  29480  omssubadd  29482  carsgcl  29486  oddpwdc  29536  eulerpartlem1  29549  eulerpartlemt  29553  eulerpartgbij  29554  eulerpartlemmf  29557  eulerpartlemgvv  29558  eulerpartlemgh  29560  eulerpartlemgs2  29562  ballotlem2  29670  ballotlemfc0  29674  ballotlemfcc  29675  ballotlemfmpn  29676  ballotlemiex  29683  ballotlemsup  29686  ballotlem7  29717  ballotth  29719  bnj21  29830  bnj110  29975  bnj1204  30127  bnj1311  30139  subfacp1lem3  30211  subfacp1lem5  30213  subfacp1lem6  30214  erdszelem2  30221  conpcon  30264  cvmliftmolem2  30311  cvmliftlem15  30327  cvmlift2lem12  30343  snmlff  30358  tfisg  30753  frinsg  30779  wlimss  30815  sltval2  30846  nodenselem4  30876  nobndlem5  30888  nofulllem5  30898  rankeq1o  31241  finminlem  31275  fnessref  31315  neibastop1  31317  neibastop2lem  31318  bj-rabtr  31901  bj-rabtrALTALT  31903  bj-rabtrAUTO  31904  bj-cmnssmnd  32096  bj-vecssmod  32103  bj-rrvecssvec  32110  icoreresf  32159  phpreu  32346  fin2so  32349  poimirlem26  32388  poimirlem31  32393  poimirlem32  32394  opnmbllem0  32398  mblfinlem1  32399  mblfinlem2  32400  ismblfin  32403  mbfposadd  32410  cnambfre  32411  cover2  32461  indexa  32481  fdc  32494  sstotbnd2  32526  sstotbnd3  32528  igenidl  32815  prnc  32819  toycom  33061  lkrlss  33183  atlatmstc  33407  atlatle  33408  glbconN  33464  linepsubN  33839  pmapssat  33846  pmaple  33848  pmapsub  33855  paddssat  33901  diass  35132  diaglbN  35145  diaintclN  35148  diassdvaN  35150  docaclN  35214  dibglbN  35256  dibintclN  35257  diclspsn  35284  dihglblem2N  35384  dih1dimatlem  35419  dihglb2  35432  dochval2  35442  dochcl  35443  dochvalr  35447  doch2val2  35454  dochss  35455  dochocss  35456  lclkr  35623  lclkrs  35629  lcdvbase  35683  lcdvbasess  35684  mapdunirnN  35740  mzpindd  36110  fiphp3d  36184  rencldnfilem  36185  irrapx1  36193  pellexlem3  36196  pellfundre  36246  pellfundge  36247  pellfundlb  36249  pellfundglb  36250  jm2.22  36363  jm2.23  36364  rpnnen3  36400  fglmod  36444  pwssplit4  36460  pwfi2f1o  36467  hbtlem6  36501  dgraalem  36517  dgraaub  36520  itgocn  36536  rgspncl  36541  rfovcnvf1od  37101  fsovfd  37109  fsovcnvlem  37110  binomcxplemdvbinom  37357  binomcxplemcvg  37358  binomcxplemnotnn0  37360  uzwo4  38029  disjf1o  38156  icof  38189  fsumsupp0  38428  limcperiod  38478  sumnnodd  38480  fnlimabslt  38529  cncfshift  38542  cncfperiod  38547  ioodvbdlimc1lem1  38604  dvnprodlem1  38619  dvnprodlem2  38620  stoweidlem14  38690  stoweidlem34  38710  stoweidlem44  38720  stoweidlem50  38726  stoweidlem51  38727  stoweidlem52  38728  stoweidlem57  38733  stoweidlem59  38735  fourierdlem19  38802  fourierdlem20  38803  fourierdlem25  38808  fourierdlem31  38814  fourierdlem37  38820  fourierdlem42  38825  fourierdlem51  38833  fourierdlem54  38836  fourierdlem64  38846  fourierdlem79  38861  elaa2lem  38909  etransclem16  38926  etransclem24  38934  etransclem31  38941  etransclem33  38943  etransclem34  38944  etransclem48  38958  rrxbasefi  38962  salgencl  39009  salexct  39011  salgenuni  39014  subsaliuncllem  39034  meadjiunlem  39141  caragenss  39177  caratheodory  39201  ovnlecvr  39231  ovnsslelem  39233  ovnlerp  39235  ovn0lem  39238  ovnsubaddlem1  39243  hoidmv1lelem1  39264  hoidmv1lelem3  39266  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  ovnhoilem1  39274  ovnhoilem2  39275  ovnlecvr2  39283  ovncvr2  39284  opnvonmbllem2  39306  ovolval4lem1  39322  ovolval5lem3  39327  pimconstlt1  39375  pimltpnf  39376  pimiooltgt  39381  pimgtmnf2  39384  pimdecfgtioc  39385  pimincfltioc  39386  pimdecfgtioo  39387  pimincfltioo  39388  sssmf  39408  incsmflem  39411  smfaddlem1  39432  smfaddlem2  39433  decsmflem  39435  smflimlem1  39440  smflimlem2  39441  smflimlem3  39442  smfrec  39457  smfmullem4  39462  smfdiv  39465  prmdvdsfmtnof1lem1  39818  prmdvdsfmtnof  39820  perfectALTVlem2  39949  incistruhgr  40286  upgrss  40295  upgrn0  40296  upgruhgr  40308  usgrss  40385  uspgrushgr  40386  ushgredgedga  40437  ushgredgedgaloop  40439  vtxdun  40677  hashwwlksnext  41101  clwwlkssswrd  41199  frcond3  41421  frgrwopreg1  41468  frgrwopreg2  41469  rabsubmgmd  41562  mgmhmeql  41574  oddibas  41584  2zlidl  41705  2zrngbas  41707  2zrng0  41709
  Copyright terms: Public domain W3C validator