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

Theorem ssrab2 4053
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 3144 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 4052 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3998 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  {cab 2796  {crab 3139  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940  df-ss 3949
This theorem is referenced by:  ssrab3  4054  ssrabeq  4056  iinrab2  4983  riinrab  4997  rabexg  5225  pwnss  5241  rabelpw  5244  frminex  5528  wereu2  5545  wfisg  6176  ssimaex  6741  f1oresrab  6881  weniso  7096  canth  7100  riotacl  7120  riotassuni  7143  onminesb  7502  onminsb  7503  onintrab  7505  onnminsb  7508  onminex  7511  tfis  7558  suppssdm  7832  fnsuppres  7846  oeeulem  8216  nnawordex  8252  pmvalg  8406  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  9415  acni3  9461  dfac2a  9543  cofsmo  9679  coftr  9683  fin2i2  9728  isfin2-2  9729  enfin2i  9731  fin1a2lem11  9820  fin1a2lem12  9821  axdc3lem4  9863  ac6num  9889  ac6  9890  ondomon  9973  alephval2  9982  pwfseqlem1  10068  pwfseqlem3  10070  wunccl  10154  tskmcl  10251  fiminreOLD  11578  infm3  11588  uzf  12234  nnwos  12303  supminf  12323  zsupss  12325  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  ixxf  12736  fzf  12884  flval3  13173  rabssnn0fi  13342  expge0  13453  expge1  13454  hashbclem  13798  sqrlem3  14592  rlimrege0  14924  incexc2  15181  bitsf  15764  bitsfzolem  15771  sadadd2lem  15796  sadadd3  15798  sadcl  15799  smupf  15815  smuval2  15819  smupvallem  15820  smucl  15821  smueqlem  15827  lcmcllem  15928  lcmn0cl  15929  lcmledvds  15931  lcmfval  15953  lcmfcllem  15957  lcmfn0cl  15958  lcmfledvds  15964  phicl2  16093  phibnd  16096  hashdvds  16100  phiprmpw  16101  phimullem  16104  eulerth  16108  phisum  16115  odzcllem  16117  odzdvds  16120  prmreclem1  16240  prmreclem2  16241  prmreclem3  16242  prmreclem4  16243  prmreclem5  16244  hashbccl  16327  prmgaplem3  16377  prmgaplem4  16378  prdsds  16725  mrcflem  16865  isacs1i  16916  wunnat  17214  dmcoass  17314  lublecl  17587  lubid  17588  issubmd  17959  mhmeql  17978  cntzval  18389  cntzssv  18396  symgsssg  18524  symgfisg  18525  pmtrdifellem4  18536  odfval  18589  odlem1  18592  odlem2  18596  odngen  18631  gexlem1  18633  gexlem2  18636  sylow2alem2  18672  sylow2blem3  18676  oddvdssubg  18904  cyggex2  18946  ablfaclem3  19138  lssacs  19668  lspf  19675  asplss  20031  aspsubrg  20033  psrass1lem  20085  psrdi  20114  psrdir  20115  psrass23l  20116  psrass23  20118  resspsrmul  20125  mplbas  20137  mplsubglem  20142  mplsubrglem  20147  mplmonmul  20173  psropprmul  20334  ocvfval  20738  ocvval  20739  dsmmval2  20808  dsmmsubg  20815  scmatlss  21062  smadiadet  21207  pmatcoe1fsupp  21237  cpmatsubgpmat  21256  fctop  21540  cctop  21542  ppttop  21543  epttop  21545  clscld  21583  neips  21649  neiptopnei  21668  ordtbaslem  21724  ordtuni  21726  ordtcld1  21733  ordtcld2  21734  cnpfval  21770  iscnp2  21775  cmpcov2  21926  cmpsublem  21935  tgcmp  21937  conncompcld  21970  1stcfb  21981  2ndc1stc  21987  2ndcdisj  21992  finlocfin  22056  kgentopon  22074  xkotf  22121  txkgen  22188  xkococnlem  22195  imastopn  22256  kqffn  22261  opnfbas  22378  flimfnfcls  22564  alexsubALT  22587  ptcmplem2  22589  symgtgp  22637  tgpconncompeqg  22647  tgpconncomp  22648  ghmcnp  22650  tsmsfbas  22663  eltsms  22668  utoptop  22770  utopbas  22771  blfvalps  22920  blfps  22943  blf  22944  nmoffn  23247  nmofval  23250  nmogelb  23252  nmolb  23253  nmof  23255  ishtpy  23503  clsocv  23780  rrxnm  23921  rrxbasefi  23940  minveclem3b  23958  minveclem4  23962  ovolcl  24006  ovollb  24007  ovolgelb  24008  ovolge0  24009  ovolshftlem1  24037  ovolshft  24039  ovolscalem1  24041  ovolscalem2  24042  ovolsca  24043  ovolicc2lem3  24047  shftmbl  24066  iundisj  24076  dyadmax  24126  dyadmbllem  24127  opnmbllem  24129  mdegmullem  24599  uc1pval  24660  mon1pval  24662  elqaalem1  24835  elqaalem3  24837  aannenlem2  24845  aalioulem2  24849  radcnvcl  24932  radcnvlt1  24933  radcnvle  24935  ftalem4  25580  ftalem5  25581  efnnfsumcl  25607  isppw  25618  sgmval2  25647  efchtdvds  25663  sqff1o  25686  fsumdvdsdiaglem  25687  fsumdvdsdiag  25688  fsumdvdscom  25689  musum  25695  muinv  25697  sgmmul  25704  ppiub  25707  vmasum  25719  logfac2  25720  perfectlem2  25733  lgsfcl  25808  lgscl  25814  lgsquadlem1  25883  lgsquadlem2  25884  rpvmasumlem  25990  mudivsum  26033  mulogsum  26035  mulog2sumlem2  26038  vmalogdivsum2  26041  logsqvma  26045  logsqvma2  26046  selberglem3  26050  selberg  26051  selberg34r  26074  pntsval2  26079  pntrlog2bndlem1  26080  tglnunirn  26261  tglnssp  26265  incistruhgr  26791  upgrss  26800  upgrn0  26801  upgruhgr  26814  usgrss  26886  uspgrushgr  26887  ushgredgedg  26938  ushgredgedgloop  26940  vtxdun  27190  vtxdginducedm1  27252  wlknwwlksnbij  27593  hashwwlksnext  27620  frcond3  27975  numclwlk1lem2  28076  ocsh  28987  spancl  29040  shsval2i  29091  ococin  29112  chsupid  29116  speccl  29603  hatomistici  30066  chpssati  30067  iundisjf  30267  aciunf1  30336  fcobijfs  30385  fpwrelmap  30395  iundisjfi  30445  cycpmco2f1  30693  cycpmco2rn  30694  cycpmco2lem1  30695  cycpmco2lem2  30696  cycpmco2lem3  30697  cycpmco2lem4  30698  cycpmco2lem5  30699  cycpmco2lem6  30700  cycpmco2lem7  30701  cycpmco2  30702  locfinreflem  31003  esumrnmpt2  31226  esumpinfval  31231  sigagensiga  31299  ldgenpisyslem1  31321  ldgenpisys  31324  measvuni  31372  imambfm  31419  dya2iocuni  31440  omscl  31452  oms0  31454  omsmon  31455  omssubadd  31457  carsgcl  31461  oddpwdc  31511  eulerpartlem1  31524  eulerpartlemt  31528  eulerpartgbij  31529  eulerpartlemmf  31532  eulerpartlemgh  31535  eulerpartlemgs2  31537  ballotlem2  31645  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemfmpn  31651  ballotlemiex  31658  ballotlemsup  31661  ballotlem7  31692  ballotth  31694  reprpmtf1o  31796  breprexplema  31800  hgt750lema  31827  bnj110  32029  bnj1204  32181  bnj1311  32193  subfacp1lem3  32326  subfacp1lem5  32328  subfacp1lem6  32329  erdszelem2  32336  connpconn  32379  cvmliftmolem2  32426  cvmliftlem15  32442  cvmlift2lem12  32458  snmlff  32473  satfrnmapom  32514  tfisg  32952  frpomin  32975  frpoinsg  32978  frinsg  32984  sltval2  33060  conway  33161  scutun12  33168  scutbdaybnd  33172  scutbdaylt  33173  rankeq1o  33529  finminlem  33563  fnessref  33602  neibastop1  33604  neibastop2lem  33605  bj-rabtr  34145  bj-rabtrAUTO  34147  bj-vecssmod  34451  icoreresf  34515  phpreu  34757  fin2so  34760  poimirlem26  34799  poimirlem31  34804  poimirlem32  34805  opnmbllem0  34809  mblfinlem1  34810  mblfinlem2  34811  ismblfin  34814  mbfposadd  34820  cnambfre  34821  cover2  34870  indexa  34889  fdc  34901  sstotbnd2  34933  sstotbnd3  34935  igenidl  35222  prnc  35226  toycom  35989  lkrlss  36111  atlatmstc  36335  atlatle  36336  glbconN  36393  linepsubN  36768  pmapssat  36775  pmaple  36777  pmapsub  36784  paddssat  36830  diass  38058  diaglbN  38071  diaintclN  38074  diassdvaN  38076  docaclN  38140  dibglbN  38182  dibintclN  38183  diclspsn  38210  dihglblem2N  38310  dih1dimatlem  38345  dihglb2  38358  dochval2  38368  dochcl  38369  dochvalr  38373  doch2val2  38380  dochss  38381  dochocss  38382  lclkr  38549  lclkrs  38555  lcdvbase  38609  lcdvbasess  38610  mapdunirnN  38666  mzpindd  39221  fiphp3d  39294  rencldnfilem  39295  irrapx1  39303  pellexlem3  39306  pellfundre  39356  pellfundge  39357  pellfundlb  39359  pellfundglb  39360  jm2.22  39470  jm2.23  39471  rpnnen3  39507  pwssplit4  39567  pwfi2f1o  39574  hbtlem6  39607  dgraalem  39623  dgraaub  39626  itgocn  39642  rgspncl  39647  rfovcnvf1od  40228  fsovfd  40236  fsovcnvlem  40237  binomcxplemdvbinom  40562  binomcxplemcvg  40563  binomcxplemnotnn0  40565  uzwo4  41192  disjf1o  41328  icof  41358  allbutfiinf  41570  supminfxr  41616  supminfxr2  41621  fsumsupp0  41735  sumnnodd  41787  fnlimabslt  41836  liminfvalxr  41940  ioodvbdlimc1lem1  42092  dvnprodlem1  42107  dvnprodlem2  42108  stoweidlem14  42176  stoweidlem34  42196  stoweidlem44  42206  stoweidlem50  42212  stoweidlem51  42213  stoweidlem52  42214  stoweidlem57  42219  stoweidlem59  42221  fourierdlem19  42288  fourierdlem20  42289  fourierdlem25  42294  fourierdlem31  42300  fourierdlem37  42306  fourierdlem42  42311  fourierdlem51  42319  fourierdlem54  42322  fourierdlem64  42332  fourierdlem79  42347  elaa2lem  42395  etransclem16  42412  etransclem24  42420  etransclem31  42427  etransclem33  42429  etransclem34  42430  etransclem48  42444  salgencl  42492  salexct  42494  salgenuni  42497  subsaliuncllem  42517  meadjiunlem  42624  caragenss  42663  caratheodory  42687  ovnlecvr  42717  ovnsslelem  42719  ovnlerp  42721  ovn0lem  42724  ovnsubaddlem1  42729  hoidmv1lelem1  42750  hoidmv1lelem3  42752  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  ovnhoilem1  42760  ovnhoilem2  42761  ovnlecvr2  42769  ovncvr2  42770  opnvonmbllem2  42792  ovolval4lem1  42808  ovolval5lem3  42813  pimconstlt1  42860  pimltpnf  42861  pimiooltgt  42866  pimgtmnf2  42869  pimdecfgtioc  42870  pimincfltioc  42871  pimdecfgtioo  42872  pimincfltioo  42873  sssmf  42892  incsmflem  42895  smfaddlem1  42916  smfaddlem2  42917  decsmflem  42919  smflimlem1  42924  smflimlem2  42925  smflimlem3  42926  smfrec  42941  smfmullem4  42946  smfdiv  42949  smfsuplem1  42962  smfsuplem3  42964  smfinflem  42968  smflimsuplem1  42971  smflimsuplem7  42977  smfliminflem  42981  sprsymrelfolem1  43531  prmdvdsfmtnof1lem1  43623  prmdvdsfmtnof  43625  perfectALTVlem2  43764  rabsubmgmd  43935  mgmhmeql  43947  oddibas  43957  2zlidl  44133  2zrngbas  44135  2zrng0  44137
  Copyright terms: Public domain W3C validator