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

Theorem ssrab2 4010
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 3118 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 4009 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3952 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 399  wcel 2112  {cab 2779  {crab 3113  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  ssrab3  4011  ssrabeq  4013  iinrab2  4958  riinrab  4972  rabexg  5201  pwnss  5218  rabelpw  5221  frminex  5503  wereu2  5520  wfisg  6155  ssimaex  6727  f1oresrab  6870  weniso  7090  canth  7094  riotacl  7114  riotassuni  7137  onminesb  7497  onminsb  7498  onintrab  7500  onnminsb  7503  onminex  7506  tfis  7553  suppssdm  7830  fnsuppres  7844  oeeulem  8214  nnawordex  8250  pmvalg  8404  fineqvlem  8720  ordtypelem3  8972  ordtypelem4  8973  ordtypelem6  8975  hartogs  8996  card2on  9006  wdom2d  9032  oemapvali  9135  tz9.12lem1  9204  tz9.12lem3  9206  rankf  9211  cardf2  9360  cardid2  9370  cardmin2  9416  acni3  9462  dfac2a  9544  cofsmo  9684  coftr  9688  fin2i2  9733  isfin2-2  9734  enfin2i  9736  fin1a2lem11  9825  fin1a2lem12  9826  axdc3lem4  9868  ac6num  9894  ac6  9895  ondomon  9978  alephval2  9987  pwfseqlem1  10073  pwfseqlem3  10075  wunccl  10159  tskmcl  10256  infm3  11591  uzf  12238  nnwos  12307  supminf  12327  zsupss  12329  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  ixxf  12740  fzf  12893  flval3  13184  rabssnn0fi  13353  expge0  13465  expge1  13466  hashbclem  13810  sqrlem3  14599  rlimrege0  14931  incexc2  15188  bitsf  15769  bitsfzolem  15776  sadadd2lem  15801  sadadd3  15803  sadcl  15804  smupf  15820  smuval2  15824  smupvallem  15825  smucl  15826  smueqlem  15832  lcmcllem  15933  lcmn0cl  15934  lcmledvds  15936  lcmfval  15958  lcmfcllem  15962  lcmfn0cl  15963  lcmfledvds  15969  phicl2  16098  phibnd  16101  hashdvds  16105  phiprmpw  16106  phimullem  16109  eulerth  16113  phisum  16120  odzcllem  16122  odzdvds  16125  prmreclem1  16245  prmreclem2  16246  prmreclem3  16247  prmreclem4  16248  prmreclem5  16249  hashbccl  16332  prmgaplem3  16382  prmgaplem4  16383  prdsds  16732  mrcflem  16872  isacs1i  16923  wunnat  17221  dmcoass  17321  lublecl  17594  lubid  17595  issubmd  17966  mhmeql  17985  cntzval  18446  cntzssv  18453  symgsssg  18590  symgfisg  18591  pmtrdifellem4  18602  odfval  18655  odlem1  18658  odlem2  18662  odngen  18697  gexlem1  18699  gexlem2  18702  sylow2alem2  18738  sylow2blem3  18742  oddvdssubg  18971  cyggex2  19013  ablfaclem3  19205  lssacs  19735  lspf  19742  ocvfval  20358  ocvval  20359  dsmmval2  20428  dsmmsubg  20435  asplss  20563  aspsubrg  20565  psrass1lem  20618  psrdi  20647  psrdir  20648  psrass23l  20649  psrass23  20651  resspsrmul  20658  mplbas  20670  mplsubglem  20675  mplsubrglem  20680  mplmonmul  20707  psropprmul  20870  scmatlss  21133  smadiadet  21278  pmatcoe1fsupp  21309  cpmatsubgpmat  21328  fctop  21612  cctop  21614  ppttop  21615  epttop  21617  clscld  21655  neips  21721  neiptopnei  21740  ordtbaslem  21796  ordtuni  21798  ordtcld1  21805  ordtcld2  21806  cnpfval  21842  iscnp2  21847  cmpcov2  21998  cmpsublem  22007  tgcmp  22009  conncompcld  22042  1stcfb  22053  2ndc1stc  22059  2ndcdisj  22064  finlocfin  22128  kgentopon  22146  xkotf  22193  txkgen  22260  xkococnlem  22267  imastopn  22328  kqffn  22333  opnfbas  22450  flimfnfcls  22636  alexsubALT  22659  ptcmplem2  22661  symgtgp  22714  tgpconncompeqg  22720  tgpconncomp  22721  ghmcnp  22723  tsmsfbas  22736  eltsms  22741  utoptop  22843  utopbas  22844  blfvalps  22993  blfps  23016  blf  23017  nmoffn  23320  nmofval  23323  nmogelb  23325  nmolb  23326  nmof  23328  ishtpy  23580  clsocv  23857  rrxnm  23998  rrxbasefi  24017  minveclem3b  24035  minveclem4  24039  ovolcl  24085  ovollb  24086  ovolgelb  24087  ovolge0  24088  ovolshftlem1  24116  ovolshft  24118  ovolscalem1  24120  ovolscalem2  24121  ovolsca  24122  ovolicc2lem3  24126  shftmbl  24145  iundisj  24155  dyadmax  24205  dyadmbllem  24206  opnmbllem  24208  mdegmullem  24682  uc1pval  24743  mon1pval  24745  elqaalem1  24918  elqaalem3  24920  aannenlem2  24928  aalioulem2  24932  radcnvcl  25015  radcnvlt1  25016  radcnvle  25018  ftalem4  25664  ftalem5  25665  efnnfsumcl  25691  isppw  25702  sgmval2  25731  efchtdvds  25747  sqff1o  25770  fsumdvdsdiaglem  25771  fsumdvdsdiag  25772  fsumdvdscom  25773  musum  25779  muinv  25781  sgmmul  25788  ppiub  25791  vmasum  25803  logfac2  25804  perfectlem2  25817  lgsfcl  25892  lgscl  25898  lgsquadlem1  25967  lgsquadlem2  25968  rpvmasumlem  26074  mudivsum  26117  mulogsum  26119  mulog2sumlem2  26122  vmalogdivsum2  26125  logsqvma  26129  logsqvma2  26130  selberglem3  26134  selberg  26135  selberg34r  26158  pntsval2  26163  pntrlog2bndlem1  26164  tglnunirn  26345  tglnssp  26349  incistruhgr  26875  upgrss  26884  upgrn0  26885  upgruhgr  26898  usgrss  26970  uspgrushgr  26971  ushgredgedg  27022  ushgredgedgloop  27024  vtxdun  27274  vtxdginducedm1  27336  wlknwwlksnbij  27677  hashwwlksnext  27703  frcond3  28057  numclwlk1lem2  28158  ocsh  29069  spancl  29122  shsval2i  29173  ococin  29194  chsupid  29198  speccl  29685  hatomistici  30148  chpssati  30149  iundisjf  30355  aciunf1  30429  fcobijfs  30488  fpwrelmap  30498  iundisjfi  30548  pwrssmgc  30709  cycpmco2f1  30819  cycpmco2rn  30820  cycpmco2lem1  30821  cycpmco2lem2  30822  cycpmco2lem3  30823  cycpmco2lem4  30824  cycpmco2lem5  30825  cycpmco2lem6  30826  cycpmco2lem7  30827  cycpmco2  30828  locfinreflem  31193  zarclsiin  31224  zarcls  31227  zartopn  31228  esumrnmpt2  31435  esumpinfval  31440  sigagensiga  31508  ldgenpisyslem1  31530  ldgenpisys  31533  measvuni  31581  imambfm  31628  dya2iocuni  31649  omscl  31661  oms0  31663  omsmon  31664  omssubadd  31666  carsgcl  31670  oddpwdc  31720  eulerpartlem1  31733  eulerpartlemt  31737  eulerpartgbij  31738  eulerpartlemmf  31741  eulerpartlemgh  31744  eulerpartlemgs2  31746  ballotlem2  31854  ballotlemfc0  31858  ballotlemfcc  31859  ballotlemfmpn  31860  ballotlemiex  31867  ballotlemsup  31870  ballotlem7  31901  ballotth  31903  reprpmtf1o  32005  breprexplema  32009  hgt750lema  32036  bnj110  32238  bnj1204  32392  bnj1311  32404  subfacp1lem3  32537  subfacp1lem5  32539  subfacp1lem6  32540  erdszelem2  32547  connpconn  32590  cvmliftmolem2  32637  cvmliftlem15  32653  cvmlift2lem12  32669  snmlff  32684  satfrnmapom  32725  tfisg  33163  frpomin  33186  frpoinsg  33189  frinsg  33195  sltval2  33271  conway  33372  scutun12  33379  scutbdaybnd  33383  scutbdaylt  33384  rankeq1o  33740  finminlem  33774  fnessref  33813  neibastop1  33815  neibastop2lem  33816  bj-rabtr  34367  bj-rabtrAUTO  34369  bj-vecssmod  34691  icoreresf  34764  phpreu  35034  fin2so  35037  poimirlem26  35076  poimirlem31  35081  poimirlem32  35082  opnmbllem0  35086  mblfinlem1  35087  mblfinlem2  35088  ismblfin  35091  mbfposadd  35097  cnambfre  35098  cover2  35145  indexa  35164  fdc  35176  sstotbnd2  35205  sstotbnd3  35207  igenidl  35494  prnc  35498  toycom  36262  lkrlss  36384  atlatmstc  36608  atlatle  36609  glbconN  36666  linepsubN  37041  pmapssat  37048  pmaple  37050  pmapsub  37057  paddssat  37103  diass  38331  diaglbN  38344  diaintclN  38347  diassdvaN  38349  docaclN  38413  dibglbN  38455  dibintclN  38456  diclspsn  38483  dihglblem2N  38583  dih1dimatlem  38618  dihglb2  38631  dochval2  38641  dochcl  38642  dochvalr  38646  doch2val2  38653  dochss  38654  dochocss  38655  lclkr  38822  lclkrs  38828  lcdvbase  38882  lcdvbasess  38883  mapdunirnN  38939  mzpindd  39674  fiphp3d  39747  rencldnfilem  39748  irrapx1  39756  pellexlem3  39759  pellfundre  39809  pellfundge  39810  pellfundlb  39812  pellfundglb  39813  jm2.22  39923  jm2.23  39924  rpnnen3  39960  pwssplit4  40020  pwfi2f1o  40027  hbtlem6  40060  dgraalem  40076  dgraaub  40079  itgocn  40095  rgspncl  40100  rfovcnvf1od  40692  fsovfd  40700  fsovcnvlem  40701  binomcxplemdvbinom  41044  binomcxplemcvg  41045  binomcxplemnotnn0  41047  uzwo4  41674  disjf1o  41805  icof  41835  allbutfiinf  42044  supminfxr  42090  supminfxr2  42095  fsumsupp0  42207  sumnnodd  42259  fnlimabslt  42308  liminfvalxr  42412  ioodvbdlimc1lem1  42560  dvnprodlem1  42575  dvnprodlem2  42576  stoweidlem14  42643  stoweidlem34  42663  stoweidlem44  42673  stoweidlem50  42679  stoweidlem51  42680  stoweidlem52  42681  stoweidlem57  42686  stoweidlem59  42688  fourierdlem19  42755  fourierdlem20  42756  fourierdlem25  42761  fourierdlem31  42767  fourierdlem37  42773  fourierdlem42  42778  fourierdlem51  42786  fourierdlem54  42789  fourierdlem64  42799  fourierdlem79  42814  elaa2lem  42862  etransclem16  42879  etransclem24  42887  etransclem31  42894  etransclem33  42896  etransclem34  42897  etransclem48  42911  salgencl  42959  salexct  42961  salgenuni  42964  subsaliuncllem  42984  meadjiunlem  43091  caragenss  43130  caratheodory  43154  ovnlecvr  43184  ovnsslelem  43186  ovnlerp  43188  ovn0lem  43191  ovnsubaddlem1  43196  hoidmv1lelem1  43217  hoidmv1lelem3  43219  hoidmvlelem1  43221  hoidmvlelem2  43222  hoidmvlelem3  43223  hoidmvlelem4  43224  ovnhoilem1  43227  ovnhoilem2  43228  ovnlecvr2  43236  ovncvr2  43237  opnvonmbllem2  43259  ovolval4lem1  43275  ovolval5lem3  43280  pimconstlt1  43327  pimltpnf  43328  pimiooltgt  43333  pimgtmnf2  43336  pimdecfgtioc  43337  pimincfltioc  43338  pimdecfgtioo  43339  pimincfltioo  43340  sssmf  43359  incsmflem  43362  smfaddlem1  43383  smfaddlem2  43384  decsmflem  43386  smflimlem1  43391  smflimlem2  43392  smflimlem3  43393  smfrec  43408  smfmullem4  43413  smfdiv  43416  smfsuplem1  43429  smfsuplem3  43431  smfinflem  43435  smflimsuplem1  43438  smflimsuplem7  43444  smfliminflem  43448  sprsymrelfolem1  43996  prmdvdsfmtnof1lem1  44088  prmdvdsfmtnof  44090  perfectALTVlem2  44227  rabsubmgmd  44398  mgmhmeql  44410  oddibas  44420  2zlidl  44545  2zrngbas  44547  2zrng0  44549
  Copyright terms: Public domain W3C validator