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

Theorem ssrab2 3884
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 3105 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 3883 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3832 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 2156  {cab 2792  {crab 3100  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-in 3776  df-ss 3783
This theorem is referenced by:  ssrab3  3885  ssrabeq  3887  iinrab2  4775  riinrab  4788  rabexg  5006  pwnss  5022  frminex  5291  wereu2  5308  dmmptss  5845  wfisg  5928  ssimaex  6484  f1oresrab  6617  weniso  6828  canth  6832  riotacl  6849  riotassuni  6872  onminesb  7228  onminsb  7229  onintrab  7231  onnminsb  7234  onminex  7237  tfis  7284  omsson  7299  suppssdm  7542  fnsuppres  7557  oawordeulem  7871  oeeulem  7918  nnawordex  7954  pmvalg  8103  fineqvlem  8413  ordtypelem2  8663  ordtypelem3  8664  ordtypelem4  8665  ordtypelem6  8667  hartogs  8688  wemapso2lem  8696  card2on  8698  wdom2d  8724  oemapvali  8828  wemapwe  8841  tz9.12lem1  8897  tz9.12lem3  8899  rankf  8904  cplem1  8999  cardf2  9052  cardid2  9062  cardmin2  9107  acni3  9153  dfac2a  9235  cofsmo  9376  coftr  9380  fin2i2  9425  isfin2-2  9426  enfin2i  9428  fin23lem28  9447  fin23lem30  9449  isf32lem5  9464  isf32lem6  9465  isf32lem7  9466  isf32lem8  9467  fin1a2lem11  9517  fin1a2lem12  9518  hsmexlem4  9536  hsmexlem5  9537  hsmexlem6  9538  axdc3lem4  9560  ac6num  9586  ac6  9587  zorn2lem1  9603  zorn2lem3  9605  zorn2lem4  9606  zorn2lem5  9607  ondomon  9670  alephval2  9679  pwfseqlem1  9765  pwfseqlem3  9767  wunccl  9851  tskmcl  9948  0nnq  10031  elpqn  10032  fiminre  11257  infm3  11267  uzf  11907  nnwos  11974  supminf  11994  zsupss  11996  rpnnen1lem2  12033  rpnnen1lem1  12034  rpnnen1lem3  12035  rpnnen1lem5  12037  rpre  12053  ixxf  12403  fzf  12553  flval3  12840  rabssnn0fi  13009  expge0  13119  expge1  13120  hashbclem  13453  sqrlem3  14208  sqrlem5  14210  rlimrege0  14533  incexc2  14792  dvdsflip  15262  divalglem2  15338  divalglem5  15340  divalglem8  15343  bitsf  15368  bitsfzolem  15375  sadadd2lem  15400  sadadd3  15402  sadcl  15403  smupf  15419  smuval2  15423  smupvallem  15424  smucl  15425  smueqlem  15431  gcdcllem3  15442  bezoutlem2  15476  bezoutlem3  15477  lcmcllem  15528  lcmn0cl  15529  lcmledvds  15531  lcmfval  15553  lcmfcllem  15557  lcmfn0cl  15558  lcmfledvds  15564  maxprmfct  15638  phicl2  15690  phibnd  15693  hashdvds  15697  phiprmpw  15698  phimullem  15701  eulerthlem2  15704  eulerth  15705  phisum  15712  odzcllem  15714  odzdvds  15717  pclem  15760  infpn2  15834  prmreclem1  15837  prmreclem2  15838  prmreclem3  15839  prmreclem4  15840  prmreclem5  15841  4sqlem13  15878  4sqlem14  15879  4sqlem17  15882  4sqlem18  15883  vdwnnlem3  15918  hashbccl  15924  ramcl2lem  15930  ramtcl  15931  ramtcl2  15932  ramtub  15933  prmgaplem3  15974  prmgaplem4  15975  prdsds  16329  imasdsval2  16381  mrcflem  16471  isacs1i  16522  wunnat  16820  dmcoass  16920  lublecl  17194  lubid  17195  gsumval1  17482  issubmd  17554  mhmeql  17569  nmzsubg  17837  nmznsg  17840  conjnmz  17896  conjnmzb  17897  gastacl  17943  cntzval  17955  cntzssv  17962  symgsssg  18088  symgfisg  18089  pmtrdifellem4  18100  odlem1  18155  odlem2  18159  odngen  18193  gexlem1  18195  gexlem2  18198  sylow1lem2  18215  sylow1lem3  18216  sylow1lem4  18217  sylow1lem5  18218  sylow2alem2  18234  sylow2a  18235  sylow2blem3  18238  sylow3lem2  18244  oddvdssubg  18459  cyggex2  18499  ablfacrplem  18666  ablfacrp2  18668  ablfac1eu  18674  pgpfaclem1  18682  ablfaclem2  18687  ablfaclem3  18688  lssacs  19174  lspf  19181  lspsolvlem  19350  lbsextlem2  19368  lbsextlem3  19369  lbsextlem4  19370  rrgeq0  19499  rrgss  19501  asplss  19538  aspsubrg  19540  psrbagconf1o  19583  psrass1lem  19586  psrdi  19615  psrdir  19616  psrass23l  19617  psrass23  19619  resspsrmul  19626  mplbas  19638  mplbasss  19641  mplsubglem  19643  mplsubrglem  19648  mplmonmul  19673  psropprmul  19816  coe1mul2lem2  19846  cygznlem2a  20123  psgnghm  20133  ocvfval  20220  ocvval  20221  dsmmbase  20289  dsmmval2  20290  dsmmsubg  20297  frlmsslsp  20345  scmatlss  20542  smadiadet  20688  pmatcoe1fsupp  20719  cpmatsubgpmat  20738  fctop  21022  cctop  21024  ppttop  21025  epttop  21027  clscld  21065  mretopd  21110  neips  21131  neiptopnei  21150  ordtbaslem  21206  ordtuni  21208  ordtcld1  21215  ordtcld2  21216  cnpfval  21252  iscnp2  21257  cmpcov2  21407  cmpsublem  21416  tgcmp  21418  hauscmplem  21423  conncompcld  21451  1stcfb  21462  2ndc1stc  21468  2ndcdisj  21473  finlocfin  21537  kgentopon  21555  xkotf  21602  txkgen  21669  xkococnlem  21676  imastopn  21737  kqffn  21742  opnfbas  21859  flimfnfcls  22045  alexsubALT  22068  ptcmplem1  22069  ptcmplem2  22070  ptcmplem3  22071  symgtgp  22118  tgpconncompeqg  22128  tgpconncomp  22129  ghmcnp  22131  tsmsfbas  22144  eltsms  22149  utoptop  22251  utopbas  22252  imasdsf1olem  22391  blfvalps  22401  blfps  22424  blf  22425  blcld  22523  nmoffn  22728  nmofval  22731  nmogelb  22733  nmolb  22734  nmof  22736  icccmplem1  22838  icccmplem2  22839  icccmplem3  22840  ishtpy  22984  clsocv  23261  rrxnm  23391  rrxf  23396  minveclem3b  23411  minveclem4  23415  ivthlem1  23432  ivthlem2  23433  ivthlem3  23434  ovolcl  23459  ovollb  23460  ovolgelb  23461  ovolge0  23462  ovolsslem  23465  ovolshftlem1  23490  ovolshft  23492  ovolscalem1  23494  ovolscalem2  23495  ovolsca  23496  ovolicc2lem3  23500  ovolicc2lem4  23501  ovolicc2lem5  23502  ovolicc2  23503  shftmbl  23519  iundisj  23529  dyadmax  23579  dyadmbllem  23580  dyadmbl  23581  opnmbllem  23582  iblmbf  23748  mdegmullem  24052  uc1pval  24113  mon1pval  24115  elqaalem1  24288  elqaalem3  24290  aannenlem2  24298  aalioulem2  24302  radcnvcl  24385  radcnvlt1  24386  radcnvle  24388  abelthlem4  24402  abelthlem6  24404  abelthlem9  24408  abelth  24409  atancn  24877  lgamucov  24978  lgamucov2  24979  ftalem3  25015  ftalem4  25016  ftalem5  25017  efnnfsumcl  25043  isppw  25054  sgmval2  25083  efchtdvds  25099  sqff1o  25122  fsumdvdsdiaglem  25123  fsumdvdsdiag  25124  fsumdvdscom  25125  musum  25131  muinv  25133  dvdsmulf1o  25134  fsumdvdsmul  25135  sgmmul  25140  ppiub  25143  vmasum  25155  logfac2  25156  perfectlem2  25169  lgsfcl2  25242  lgsfcl  25244  lgscl  25250  lgsquadlem1  25319  lgsquadlem2  25320  rpvmasumlem  25390  rpvmasum2  25415  dchrisum0re  25416  dchrisum0lema  25417  dchrisum0lem1b  25418  dchrisum0lem1  25419  dchrisum0lem2a  25420  dchrisum0lem2  25421  dchrisum0lem3  25422  dchrisum0  25423  mudivsum  25433  mulogsum  25435  mulog2sumlem2  25438  vmalogdivsum2  25441  logsqvma  25445  logsqvma2  25446  selberglem3  25450  selberg  25451  selberg34r  25474  pntsval2  25479  pntrlog2bndlem1  25480  pntlem3  25512  tglnunirn  25657  tglnssp  25661  axcontlem2  26059  axcontlem7  26064  axcontlem8  26065  axcontlem10  26067  incistruhgr  26188  upgrss  26197  upgrn0  26198  upgruhgr  26211  usgrss  26284  uspgrushgr  26285  ushgredgedg  26336  ushgredgedgloop  26338  ushgredgedgloopOLD  26339  upgrreslem  26412  umgrreslem  26413  vtxdun  26605  vtxdginducedm1lem2  26664  vtxdginducedm1  26667  finsumvtxdg2ssteplem1  26669  wlknwwlksnbij  27019  hashwwlksnext  27052  clwwlksswrd  27130  frcond3  27444  numclwlk1lem2  27550  ocsh  28470  spancl  28523  shsval2i  28574  ococin  28595  chsupid  28599  speccl  29086  atssch  29530  hatomistici  29549  chpssati  29550  iundisjf  29727  aciunf1  29790  fcobijfs  29828  fpwrelmap  29835  iundisjfi  29882  locfinreflem  30232  esumrnmpt2  30455  esumpinfval  30460  sigagensiga  30529  ldgenpisyslem1  30551  ldgenpisys  30554  measvuni  30602  imambfm  30649  dya2iocuni  30670  omscl  30682  oms0  30684  omsmon  30685  omssubadd  30687  carsgcl  30691  oddpwdc  30741  eulerpartlem1  30754  eulerpartlemt  30758  eulerpartgbij  30759  eulerpartlemmf  30762  eulerpartlemgh  30765  eulerpartlemgs2  30767  ballotlem2  30875  ballotlemfc0  30879  ballotlemfcc  30880  ballotlemfmpn  30881  ballotlemiex  30888  ballotlemsup  30891  ballotlem7  30922  ballotth  30924  reprpmtf1o  31029  breprexplema  31033  hgt750lema  31060  bnj110  31251  bnj1204  31403  bnj1311  31415  subfacp1lem3  31487  subfacp1lem5  31489  subfacp1lem6  31490  erdszelem2  31497  connpconn  31540  cvmliftmolem2  31587  cvmliftlem15  31603  cvmlift2lem12  31619  snmlff  31634  tfisg  32036  frpomin  32059  frpoinsg  32062  frinsg  32066  wlimss  32095  sltval2  32130  conway  32231  scutun12  32238  scutbdaybnd  32242  scutbdaylt  32243  rankeq1o  32599  finminlem  32633  fnessref  32673  neibastop1  32675  neibastop2lem  32676  bj-rabtr  33237  bj-rabtrALTALT  33239  bj-rabtrAUTO  33240  bj-cmnssmnd  33453  bj-vecssmod  33460  bj-rrvecssvec  33467  icoreresf  33516  phpreu  33706  fin2so  33709  poimirlem26  33748  poimirlem31  33753  poimirlem32  33754  opnmbllem0  33758  mblfinlem1  33759  mblfinlem2  33760  ismblfin  33763  mbfposadd  33769  cnambfre  33770  cover2  33820  indexa  33840  fdc  33852  sstotbnd2  33884  sstotbnd3  33886  igenidl  34173  prnc  34177  toycom  34753  lkrlss  34875  atlatmstc  35099  atlatle  35100  glbconN  35157  linepsubN  35532  pmapssat  35539  pmaple  35541  pmapsub  35548  paddssat  35594  diass  36823  diaglbN  36836  diaintclN  36839  diassdvaN  36841  docaclN  36905  dibglbN  36947  dibintclN  36948  diclspsn  36975  dihglblem2N  37075  dih1dimatlem  37110  dihglb2  37123  dochval2  37133  dochcl  37134  dochvalr  37138  doch2val2  37145  dochss  37146  dochocss  37147  lclkr  37314  lclkrs  37320  lcdvbase  37374  lcdvbasess  37375  mapdunirnN  37431  mzpindd  37811  fiphp3d  37885  rencldnfilem  37886  irrapx1  37894  pellexlem3  37897  pellfundre  37947  pellfundge  37948  pellfundlb  37950  pellfundglb  37951  jm2.22  38063  jm2.23  38064  rpnnen3  38100  fglmod  38144  pwssplit4  38160  pwfi2f1o  38167  hbtlem6  38200  dgraalem  38216  dgraaub  38219  itgocn  38235  rgspncl  38240  rfovcnvf1od  38798  fsovfd  38806  fsovcnvlem  38807  binomcxplemdvbinom  39052  binomcxplemcvg  39053  binomcxplemnotnn0  39055  uzwo4  39714  disjf1o  39867  icof  39898  allbutfiinf  40126  supminfxr  40173  supminfxr2  40178  fsumsupp0  40290  sumnnodd  40342  fnlimabslt  40391  liminfvalxr  40495  ioodvbdlimc1lem1  40626  dvnprodlem1  40641  dvnprodlem2  40642  stoweidlem14  40710  stoweidlem34  40730  stoweidlem44  40740  stoweidlem50  40746  stoweidlem51  40747  stoweidlem52  40748  stoweidlem57  40753  stoweidlem59  40755  fourierdlem19  40822  fourierdlem20  40823  fourierdlem25  40828  fourierdlem31  40834  fourierdlem37  40840  fourierdlem42  40845  fourierdlem51  40853  fourierdlem54  40856  fourierdlem64  40866  fourierdlem79  40881  elaa2lem  40929  etransclem16  40946  etransclem24  40954  etransclem31  40961  etransclem33  40963  etransclem34  40964  etransclem48  40978  rrxbasefi  40982  salgencl  41029  salexct  41031  salgenuni  41034  subsaliuncllem  41054  meadjiunlem  41161  caragenss  41200  caratheodory  41224  ovnlecvr  41254  ovnsslelem  41256  ovnlerp  41258  ovn0lem  41261  ovnsubaddlem1  41266  hoidmv1lelem1  41287  hoidmv1lelem3  41289  hoidmvlelem1  41291  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  ovnhoilem1  41297  ovnhoilem2  41298  ovnlecvr2  41306  ovncvr2  41307  opnvonmbllem2  41329  ovolval4lem1  41345  ovolval5lem3  41350  pimconstlt1  41397  pimltpnf  41398  pimiooltgt  41403  pimgtmnf2  41406  pimdecfgtioc  41407  pimincfltioc  41408  pimdecfgtioo  41409  pimincfltioo  41410  sssmf  41429  incsmflem  41432  smfaddlem1  41453  smfaddlem2  41454  decsmflem  41456  smflimlem1  41461  smflimlem2  41462  smflimlem3  41463  smfrec  41478  smfmullem4  41483  smfdiv  41486  smfsuplem1  41499  smfsuplem3  41501  smfinflem  41505  smflimsuplem1  41508  smflimsuplem7  41514  smfliminflem  41518  prmdvdsfmtnof1lem1  42071  prmdvdsfmtnof  42073  perfectALTVlem2  42206  sprsymrelfolem1  42310  rabsubmgmd  42359  mgmhmeql  42371  oddibas  42381  2zlidl  42502  2zrngbas  42504  2zrng0  42506
  Copyright terms: Public domain W3C validator