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

Theorem ssrab2 3679
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 2918 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 3678 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3627 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 1988  {cab 2606  {crab 2913  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-in 3574  df-ss 3581
This theorem is referenced by:  ssrab3  3680  ssrabeq  3681  iinrab2  4574  riinrab  4587  rabexg  4803  pwnss  4821  frminex  5084  wereu2  5101  dmmptss  5619  wfisg  5703  ssimaex  6250  f1oresrab  6381  weniso  6589  canth  6593  riotacl  6610  riotassuni  6633  onminesb  6983  onminsb  6984  onintrab  6986  onnminsb  6989  onminex  6992  tfis  7039  omsson  7054  suppssdm  7293  fnsuppres  7307  oawordeulem  7619  oeeulem  7666  nnawordex  7702  pmvalg  7853  fineqvlem  8159  ordtypelem2  8409  ordtypelem3  8410  ordtypelem4  8411  ordtypelem6  8413  hartogs  8434  wemapso2lem  8442  card2on  8444  wdom2d  8470  oemapvali  8566  wemapwe  8579  tz9.12lem1  8635  tz9.12lem3  8637  rankf  8642  cplem1  8737  cardf2  8754  cardid2  8764  cardmin2  8809  acni3  8855  dfac2a  8937  cofsmo  9076  coftr  9080  fin2i2  9125  isfin2-2  9126  enfin2i  9128  fin23lem28  9147  fin23lem30  9149  isf32lem5  9164  isf32lem6  9165  isf32lem7  9166  isf32lem8  9167  fin1a2lem11  9217  fin1a2lem12  9218  hsmexlem4  9236  hsmexlem5  9237  hsmexlem6  9238  axdc3lem4  9260  ac6num  9286  ac6  9287  zorn2lem1  9303  zorn2lem3  9305  zorn2lem4  9306  zorn2lem5  9307  ondomon  9370  alephval2  9379  pwfseqlem1  9465  pwfseqlem3  9467  wunccl  9551  tskmcl  9648  0nnq  9731  elpqn  9732  fiminre  10957  infm3  10967  uzf  11675  nnwos  11740  supminf  11760  zsupss  11762  rpnnen1lem2  11799  rpnnen1lem1  11800  rpnnen1lem3  11801  rpnnen1lem5  11803  rpnnen1lem1OLD  11806  rpnnen1lem3OLD  11807  rpnnen1lem5OLD  11809  rpre  11824  ixxf  12170  fzf  12315  flval3  12599  rabssnn0fi  12768  expge0  12879  expge1  12880  hashbclem  13219  sqrlem3  13966  sqrlem5  13968  rlimrege0  14291  incexc2  14551  dvdsflip  15020  divalglem2  15099  divalglem5  15101  divalglem8  15104  bitsf  15130  bitsfzolem  15137  sadadd2lem  15162  sadadd3  15164  sadcl  15165  smupf  15181  smuval2  15185  smupvallem  15186  smucl  15187  smueqlem  15193  gcdcllem3  15204  bezoutlem2  15238  bezoutlem3  15239  lcmcllem  15290  lcmn0cl  15291  lcmledvds  15293  lcmfval  15315  lcmfcllem  15319  lcmfn0cl  15320  lcmfledvds  15326  maxprmfct  15402  phicl2  15454  phibnd  15457  hashdvds  15461  phiprmpw  15462  phimullem  15465  eulerthlem2  15468  eulerth  15469  phisum  15476  odzcllem  15478  odzdvds  15481  pclem  15524  infpn2  15598  prmreclem1  15601  prmreclem2  15602  prmreclem3  15603  prmreclem4  15604  prmreclem5  15605  4sqlem13  15642  4sqlem14  15643  4sqlem17  15646  4sqlem18  15647  vdwnnlem3  15682  hashbccl  15688  ramcl2lem  15694  ramtcl  15695  ramtcl2  15696  ramtub  15697  prmgaplem3  15738  prmgaplem4  15739  prdsds  16105  imasdsval2  16157  mrcflem  16247  isacs1i  16299  wunnat  16597  dmcoass  16697  lublecl  16970  lubid  16971  gsumval1  17258  issubmd  17330  mhmeql  17345  nmzsubg  17616  nmznsg  17619  conjnmz  17675  conjnmzb  17676  gastacl  17723  cntzval  17735  cntzssv  17742  symgsssg  17868  symgfisg  17869  pmtrdifellem4  17880  odlem1  17935  odlem2  17939  odngen  17973  gexlem1  17975  gexlem2  17978  sylow1lem2  17995  sylow1lem3  17996  sylow1lem4  17997  sylow1lem5  17998  sylow2alem2  18014  sylow2a  18015  sylow2blem3  18018  sylow3lem2  18024  oddvdssubg  18239  cyggex2  18279  ablfacrplem  18445  ablfacrp2  18447  ablfac1eu  18453  pgpfaclem1  18461  ablfaclem2  18466  ablfaclem3  18467  lssacs  18948  lspf  18955  lspsolvlem  19123  lbsextlem2  19140  lbsextlem3  19141  lbsextlem4  19142  rrgeq0  19271  rrgss  19273  asplss  19310  aspsubrg  19312  psrbagconf1o  19355  psrass1lem  19358  psrdi  19387  psrdir  19388  psrass23l  19389  psrass23  19391  resspsrmul  19398  mplbas  19410  mplbasss  19413  mplsubglem  19415  mplsubrglem  19420  mplmonmul  19445  psropprmul  19589  coe1mul2lem2  19619  cygznlem2a  19897  psgnghm  19907  ocvfval  19991  ocvval  19992  dsmmbase  20060  dsmmval2  20061  dsmmsubg  20068  frlmsslsp  20116  scmatlss  20312  smadiadet  20457  pmatcoe1fsupp  20487  cpmatsubgpmat  20506  fctop  20789  cctop  20791  ppttop  20792  epttop  20794  clscld  20832  mretopd  20877  neips  20898  neiptopnei  20917  ordtbaslem  20973  ordtuni  20975  ordtcld1  20982  ordtcld2  20983  cnpfval  21019  iscnp2  21024  cmpcov2  21174  cmpsublem  21183  tgcmp  21185  hauscmplem  21190  conncompcld  21218  1stcfb  21229  2ndc1stc  21235  2ndcdisj  21240  finlocfin  21304  kgentopon  21322  xkotf  21369  txkgen  21436  xkococnlem  21443  imastopn  21504  kqffn  21509  opnfbas  21627  flimfnfcls  21813  alexsubALT  21836  ptcmplem1  21837  ptcmplem2  21838  ptcmplem3  21839  symgtgp  21886  tgpconncompeqg  21896  tgpconncomp  21897  ghmcnp  21899  tsmsfbas  21912  eltsms  21917  utoptop  22019  utopbas  22020  imasdsf1olem  22159  blfvalps  22169  blfps  22192  blf  22193  blcld  22291  nmoffn  22496  nmofval  22499  nmogelb  22501  nmolb  22502  nmof  22504  icccmplem1  22606  icccmplem2  22607  icccmplem3  22608  ishtpy  22752  clsocv  23030  rrxnm  23160  rrxf  23165  minveclem3b  23180  minveclem4  23184  ivthlem1  23201  ivthlem2  23202  ivthlem3  23203  ovolcl  23227  ovollb  23228  ovolgelb  23229  ovolge0  23230  ovolsslem  23233  ovolshftlem1  23258  ovolshft  23260  ovolscalem1  23262  ovolscalem2  23263  ovolsca  23264  ovolicc2lem3  23268  ovolicc2lem4  23269  ovolicc2lem5  23270  ovolicc2  23271  shftmbl  23287  iundisj  23297  dyadmax  23347  dyadmbllem  23348  dyadmbl  23349  opnmbllem  23350  iblmbf  23515  mdegmullem  23819  uc1pval  23880  mon1pval  23882  elqaalem1  24055  elqaalem3  24057  aannenlem2  24065  aalioulem2  24069  radcnvcl  24152  radcnvlt1  24153  radcnvle  24155  abelthlem4  24169  abelthlem6  24171  abelthlem9  24175  abelth  24176  atancn  24644  lgamucov  24745  lgamucov2  24746  ftalem3  24782  ftalem4  24783  ftalem5  24784  efnnfsumcl  24810  isppw  24821  sgmval2  24850  efchtdvds  24866  sqff1o  24889  fsumdvdsdiaglem  24890  fsumdvdsdiag  24891  fsumdvdscom  24892  musum  24898  muinv  24900  dvdsmulf1o  24901  fsumdvdsmul  24902  sgmmul  24907  ppiub  24910  vmasum  24922  logfac2  24923  perfectlem2  24936  lgsfcl2  25009  lgsfcl  25011  lgscl  25017  lgsquadlem1  25086  lgsquadlem2  25087  rpvmasumlem  25157  rpvmasum2  25182  dchrisum0re  25183  dchrisum0lema  25184  dchrisum0lem1b  25185  dchrisum0lem1  25186  dchrisum0lem2a  25187  dchrisum0lem2  25188  dchrisum0lem3  25189  dchrisum0  25190  mudivsum  25200  mulogsum  25202  mulog2sumlem2  25205  vmalogdivsum2  25208  logsqvma  25212  logsqvma2  25213  selberglem3  25217  selberg  25218  selberg34r  25241  pntsval2  25246  pntrlog2bndlem1  25247  pntlem3  25279  tglnunirn  25424  tglnssp  25428  axcontlem2  25826  axcontlem7  25831  axcontlem8  25832  axcontlem10  25834  incistruhgr  25955  upgrss  25964  upgrn0  25965  upgruhgr  25978  usgrss  26050  uspgrushgr  26051  ushgredgedg  26102  ushgredgedgloop  26104  upgrreslem  26177  umgrreslem  26178  vtxdun  26358  vtxdginducedm1lem2  26417  vtxdginducedm1  26420  finsumvtxdg2ssteplem1  26422  hashwwlksnext  26790  clwwlkssswrd  26891  frcond3  27113  frgrwopreg1  27160  ocsh  28112  spancl  28165  shsval2i  28216  ococin  28237  chsupid  28241  speccl  28728  atssch  29172  hatomistici  29191  chpssati  29192  iundisjf  29374  aciunf1  29436  fcobijfs  29475  fpwrelmap  29482  iundisjfi  29529  locfinreflem  29881  esumrnmpt2  30104  esumpinfval  30109  sigagensiga  30178  ldgenpisyslem1  30200  ldgenpisys  30203  measvuni  30251  imambfm  30298  dya2iocuni  30319  omscl  30331  oms0  30333  omsmon  30334  omssubadd  30336  carsgcl  30340  oddpwdc  30390  eulerpartlem1  30403  eulerpartlemt  30407  eulerpartgbij  30408  eulerpartlemmf  30411  eulerpartlemgvv  30412  eulerpartlemgh  30414  eulerpartlemgs2  30416  ballotlem2  30524  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemfmpn  30530  ballotlemiex  30537  ballotlemsup  30540  ballotlem7  30571  ballotth  30573  reprpmtf1o  30678  breprexplema  30682  hgt750lema  30709  bnj110  30902  bnj1204  31054  bnj1311  31066  subfacp1lem3  31138  subfacp1lem5  31140  subfacp1lem6  31141  erdszelem2  31148  connpconn  31191  cvmliftmolem2  31238  cvmliftlem15  31254  cvmlift2lem12  31270  snmlff  31285  tfisg  31690  frinsg  31716  wlimss  31752  sltval2  31783  conway  31884  scutun12  31891  scutbdaybnd  31895  scutbdaylt  31896  rankeq1o  32253  finminlem  32287  fnessref  32327  neibastop1  32329  neibastop2lem  32330  bj-rabtr  32901  bj-rabtrALTALT  32903  bj-rabtrAUTO  32904  bj-cmnssmnd  33107  bj-vecssmod  33114  bj-rrvecssvec  33121  icoreresf  33171  phpreu  33364  fin2so  33367  poimirlem26  33406  poimirlem31  33411  poimirlem32  33412  opnmbllem0  33416  mblfinlem1  33417  mblfinlem2  33418  ismblfin  33421  mbfposadd  33428  cnambfre  33429  cover2  33479  indexa  33499  fdc  33512  sstotbnd2  33544  sstotbnd3  33546  igenidl  33833  prnc  33837  toycom  34079  lkrlss  34201  atlatmstc  34425  atlatle  34426  glbconN  34482  linepsubN  34857  pmapssat  34864  pmaple  34866  pmapsub  34873  paddssat  34919  diass  36150  diaglbN  36163  diaintclN  36166  diassdvaN  36168  docaclN  36232  dibglbN  36274  dibintclN  36275  diclspsn  36302  dihglblem2N  36402  dih1dimatlem  36437  dihglb2  36450  dochval2  36460  dochcl  36461  dochvalr  36465  doch2val2  36472  dochss  36473  dochocss  36474  lclkr  36641  lclkrs  36647  lcdvbase  36701  lcdvbasess  36702  mapdunirnN  36758  mzpindd  37128  fiphp3d  37202  rencldnfilem  37203  irrapx1  37211  pellexlem3  37214  pellfundre  37264  pellfundge  37265  pellfundlb  37267  pellfundglb  37268  jm2.22  37381  jm2.23  37382  rpnnen3  37418  fglmod  37462  pwssplit4  37478  pwfi2f1o  37485  hbtlem6  37518  dgraalem  37534  dgraaub  37537  itgocn  37553  rgspncl  37558  rfovcnvf1od  38118  fsovfd  38126  fsovcnvlem  38127  binomcxplemdvbinom  38372  binomcxplemcvg  38373  binomcxplemnotnn0  38375  uzwo4  39041  disjf1o  39194  icof  39227  allbutfiinf  39460  supminfxr  39507  supminfxr2  39512  fsumsupp0  39610  limcperiod  39660  sumnnodd  39662  fnlimabslt  39711  liminfvalxr  39809  cncfshift  39850  cncfperiod  39855  ioodvbdlimc1lem1  39909  dvnprodlem1  39924  dvnprodlem2  39925  stoweidlem14  39994  stoweidlem34  40014  stoweidlem44  40024  stoweidlem50  40030  stoweidlem51  40031  stoweidlem52  40032  stoweidlem57  40037  stoweidlem59  40039  fourierdlem19  40106  fourierdlem20  40107  fourierdlem25  40112  fourierdlem31  40118  fourierdlem37  40124  fourierdlem42  40129  fourierdlem51  40137  fourierdlem54  40140  fourierdlem64  40150  fourierdlem79  40165  elaa2lem  40213  etransclem16  40230  etransclem24  40238  etransclem31  40245  etransclem33  40247  etransclem34  40248  etransclem48  40262  rrxbasefi  40266  salgencl  40313  salexct  40315  salgenuni  40318  subsaliuncllem  40338  meadjiunlem  40445  caragenss  40481  caratheodory  40505  ovnlecvr  40535  ovnsslelem  40537  ovnlerp  40539  ovn0lem  40542  ovnsubaddlem1  40547  hoidmv1lelem1  40568  hoidmv1lelem3  40570  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem3  40574  hoidmvlelem4  40575  ovnhoilem1  40578  ovnhoilem2  40579  ovnlecvr2  40587  ovncvr2  40588  opnvonmbllem2  40610  ovolval4lem1  40626  ovolval5lem3  40631  pimconstlt1  40678  pimltpnf  40679  pimiooltgt  40684  pimgtmnf2  40687  pimdecfgtioc  40688  pimincfltioc  40689  pimdecfgtioo  40690  pimincfltioo  40691  sssmf  40710  incsmflem  40713  smfaddlem1  40734  smfaddlem2  40735  decsmflem  40737  smflimlem1  40742  smflimlem2  40743  smflimlem3  40744  smfrec  40759  smfmullem4  40764  smfdiv  40767  smfsuplem1  40780  smfsuplem3  40782  smfinflem  40786  smflimsuplem1  40789  smflimsuplem7  40795  smfliminflem  40799  prmdvdsfmtnof1lem1  41261  prmdvdsfmtnof  41263  perfectALTVlem2  41396  sprsymrelfolem1  41507  rabsubmgmd  41556  mgmhmeql  41568  oddibas  41578  2zlidl  41699  2zrngbas  41701  2zrng0  41703
  Copyright terms: Public domain W3C validator