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

Theorem ssrab2 4055
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 3147 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 4054 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 4000 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  {cab 2799  {crab 3142  wss 3935
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3942  df-ss 3951
This theorem is referenced by:  ssrab3  4056  ssrabeq  4058  iinrab2  4984  riinrab  4998  rabexg  5226  pwnss  5242  rabelpw  5245  frminex  5529  wereu2  5546  wfisg  6177  ssimaex  6742  f1oresrab  6882  weniso  7096  canth  7100  riotacl  7120  riotassuni  7143  onminesb  7501  onminsb  7502  onintrab  7504  onnminsb  7507  onminex  7510  tfis  7557  suppssdm  7834  fnsuppres  7848  oeeulem  8217  nnawordex  8253  pmvalg  8407  fineqvlem  8721  ordtypelem3  8973  ordtypelem4  8974  ordtypelem6  8976  hartogs  8997  card2on  9007  wdom2d  9033  oemapvali  9136  tz9.12lem1  9205  tz9.12lem3  9207  rankf  9212  cardf2  9361  cardid2  9371  cardmin2  9416  acni3  9462  dfac2a  9544  cofsmo  9680  coftr  9684  fin2i2  9729  isfin2-2  9730  enfin2i  9732  fin1a2lem11  9821  fin1a2lem12  9822  axdc3lem4  9864  ac6num  9890  ac6  9891  ondomon  9974  alephval2  9983  pwfseqlem1  10069  pwfseqlem3  10071  wunccl  10155  tskmcl  10252  fiminreOLD  11579  infm3  11589  uzf  12235  nnwos  12304  supminf  12324  zsupss  12326  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  ixxf  12738  fzf  12886  flval3  13175  rabssnn0fi  13344  expge0  13455  expge1  13456  hashbclem  13800  sqrlem3  14594  rlimrege0  14926  incexc2  15183  bitsf  15766  bitsfzolem  15773  sadadd2lem  15798  sadadd3  15800  sadcl  15801  smupf  15817  smuval2  15821  smupvallem  15822  smucl  15823  smueqlem  15829  lcmcllem  15930  lcmn0cl  15931  lcmledvds  15933  lcmfval  15955  lcmfcllem  15959  lcmfn0cl  15960  lcmfledvds  15966  phicl2  16095  phibnd  16098  hashdvds  16102  phiprmpw  16103  phimullem  16106  eulerth  16110  phisum  16117  odzcllem  16119  odzdvds  16122  prmreclem1  16242  prmreclem2  16243  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  hashbccl  16329  prmgaplem3  16379  prmgaplem4  16380  prdsds  16727  mrcflem  16867  isacs1i  16918  wunnat  17216  dmcoass  17316  lublecl  17589  lubid  17590  issubmd  17961  mhmeql  17980  cntzval  18391  cntzssv  18398  symgsssg  18526  symgfisg  18527  pmtrdifellem4  18538  odfval  18591  odlem1  18594  odlem2  18598  odngen  18633  gexlem1  18635  gexlem2  18638  sylow2alem2  18674  sylow2blem3  18678  oddvdssubg  18906  cyggex2  18948  ablfaclem3  19140  lssacs  19670  lspf  19677  asplss  20033  aspsubrg  20035  psrass1lem  20087  psrdi  20116  psrdir  20117  psrass23l  20118  psrass23  20120  resspsrmul  20127  mplbas  20139  mplsubglem  20144  mplsubrglem  20149  mplmonmul  20175  psropprmul  20336  ocvfval  20740  ocvval  20741  dsmmval2  20810  dsmmsubg  20817  scmatlss  21064  smadiadet  21209  pmatcoe1fsupp  21239  cpmatsubgpmat  21258  fctop  21542  cctop  21544  ppttop  21545  epttop  21547  clscld  21585  neips  21651  neiptopnei  21670  ordtbaslem  21726  ordtuni  21728  ordtcld1  21735  ordtcld2  21736  cnpfval  21772  iscnp2  21777  cmpcov2  21928  cmpsublem  21937  tgcmp  21939  conncompcld  21972  1stcfb  21983  2ndc1stc  21989  2ndcdisj  21994  finlocfin  22058  kgentopon  22076  xkotf  22123  txkgen  22190  xkococnlem  22197  imastopn  22258  kqffn  22263  opnfbas  22380  flimfnfcls  22566  alexsubALT  22589  ptcmplem2  22591  symgtgp  22639  tgpconncompeqg  22649  tgpconncomp  22650  ghmcnp  22652  tsmsfbas  22665  eltsms  22670  utoptop  22772  utopbas  22773  blfvalps  22922  blfps  22945  blf  22946  nmoffn  23249  nmofval  23252  nmogelb  23254  nmolb  23255  nmof  23257  ishtpy  23505  clsocv  23782  rrxnm  23923  rrxbasefi  23942  minveclem3b  23960  minveclem4  23964  ovolcl  24008  ovollb  24009  ovolgelb  24010  ovolge0  24011  ovolshftlem1  24039  ovolshft  24041  ovolscalem1  24043  ovolscalem2  24044  ovolsca  24045  ovolicc2lem3  24049  shftmbl  24068  iundisj  24078  dyadmax  24128  dyadmbllem  24129  opnmbllem  24131  mdegmullem  24601  uc1pval  24662  mon1pval  24664  elqaalem1  24837  elqaalem3  24839  aannenlem2  24847  aalioulem2  24851  radcnvcl  24934  radcnvlt1  24935  radcnvle  24937  ftalem4  25581  ftalem5  25582  efnnfsumcl  25608  isppw  25619  sgmval2  25648  efchtdvds  25664  sqff1o  25687  fsumdvdsdiaglem  25688  fsumdvdsdiag  25689  fsumdvdscom  25690  musum  25696  muinv  25698  sgmmul  25705  ppiub  25708  vmasum  25720  logfac2  25721  perfectlem2  25734  lgsfcl  25809  lgscl  25815  lgsquadlem1  25884  lgsquadlem2  25885  rpvmasumlem  25991  mudivsum  26034  mulogsum  26036  mulog2sumlem2  26039  vmalogdivsum2  26042  logsqvma  26046  logsqvma2  26047  selberglem3  26051  selberg  26052  selberg34r  26075  pntsval2  26080  pntrlog2bndlem1  26081  tglnunirn  26262  tglnssp  26266  incistruhgr  26792  upgrss  26801  upgrn0  26802  upgruhgr  26815  usgrss  26887  uspgrushgr  26888  ushgredgedg  26939  ushgredgedgloop  26941  vtxdun  27191  vtxdginducedm1  27253  wlknwwlksnbij  27594  hashwwlksnext  27621  frcond3  27976  numclwlk1lem2  28077  ocsh  28988  spancl  29041  shsval2i  29092  ococin  29113  chsupid  29117  speccl  29604  hatomistici  30067  chpssati  30068  iundisjf  30268  aciunf1  30337  fcobijfs  30386  fpwrelmap  30396  iundisjfi  30446  cycpmco2f1  30694  cycpmco2rn  30695  cycpmco2lem1  30696  cycpmco2lem2  30697  cycpmco2lem3  30698  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2lem7  30702  cycpmco2  30703  locfinreflem  31004  esumrnmpt2  31227  esumpinfval  31232  sigagensiga  31300  ldgenpisyslem1  31322  ldgenpisys  31325  measvuni  31373  imambfm  31420  dya2iocuni  31441  omscl  31453  oms0  31455  omsmon  31456  omssubadd  31458  carsgcl  31462  oddpwdc  31512  eulerpartlem1  31525  eulerpartlemt  31529  eulerpartgbij  31530  eulerpartlemmf  31533  eulerpartlemgh  31536  eulerpartlemgs2  31538  ballotlem2  31646  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemfmpn  31652  ballotlemiex  31659  ballotlemsup  31662  ballotlem7  31693  ballotth  31695  reprpmtf1o  31797  breprexplema  31801  hgt750lema  31828  bnj110  32030  bnj1204  32182  bnj1311  32194  subfacp1lem3  32327  subfacp1lem5  32329  subfacp1lem6  32330  erdszelem2  32337  connpconn  32380  cvmliftmolem2  32427  cvmliftlem15  32443  cvmlift2lem12  32459  snmlff  32474  satfrnmapom  32515  tfisg  32953  frpomin  32976  frpoinsg  32979  frinsg  32985  sltval2  33061  conway  33162  scutun12  33169  scutbdaybnd  33173  scutbdaylt  33174  rankeq1o  33530  finminlem  33564  fnessref  33603  neibastop1  33605  neibastop2lem  33606  bj-rabtr  34146  bj-rabtrAUTO  34148  bj-vecssmod  34452  icoreresf  34516  phpreu  34758  fin2so  34761  poimirlem26  34800  poimirlem31  34805  poimirlem32  34806  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  ismblfin  34815  mbfposadd  34821  cnambfre  34822  cover2  34872  indexa  34891  fdc  34903  sstotbnd2  34935  sstotbnd3  34937  igenidl  35224  prnc  35228  toycom  35991  lkrlss  36113  atlatmstc  36337  atlatle  36338  glbconN  36395  linepsubN  36770  pmapssat  36777  pmaple  36779  pmapsub  36786  paddssat  36832  diass  38060  diaglbN  38073  diaintclN  38076  diassdvaN  38078  docaclN  38142  dibglbN  38184  dibintclN  38185  diclspsn  38212  dihglblem2N  38312  dih1dimatlem  38347  dihglb2  38360  dochval2  38370  dochcl  38371  dochvalr  38375  doch2val2  38382  dochss  38383  dochocss  38384  lclkr  38551  lclkrs  38557  lcdvbase  38611  lcdvbasess  38612  mapdunirnN  38668  mzpindd  39223  fiphp3d  39296  rencldnfilem  39297  irrapx1  39305  pellexlem3  39308  pellfundre  39358  pellfundge  39359  pellfundlb  39361  pellfundglb  39362  jm2.22  39472  jm2.23  39473  rpnnen3  39509  pwssplit4  39569  pwfi2f1o  39576  hbtlem6  39609  dgraalem  39625  dgraaub  39628  itgocn  39644  rgspncl  39649  rfovcnvf1od  40230  fsovfd  40238  fsovcnvlem  40239  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemnotnn0  40568  uzwo4  41195  disjf1o  41332  icof  41362  allbutfiinf  41574  supminfxr  41620  supminfxr2  41625  fsumsupp0  41739  sumnnodd  41791  fnlimabslt  41840  liminfvalxr  41944  ioodvbdlimc1lem1  42096  dvnprodlem1  42111  dvnprodlem2  42112  stoweidlem14  42180  stoweidlem34  42200  stoweidlem44  42210  stoweidlem50  42216  stoweidlem51  42217  stoweidlem52  42218  stoweidlem57  42223  stoweidlem59  42225  fourierdlem19  42292  fourierdlem20  42293  fourierdlem25  42298  fourierdlem31  42304  fourierdlem37  42310  fourierdlem42  42315  fourierdlem51  42323  fourierdlem54  42326  fourierdlem64  42336  fourierdlem79  42351  elaa2lem  42399  etransclem16  42416  etransclem24  42424  etransclem31  42431  etransclem33  42433  etransclem34  42434  etransclem48  42448  salgencl  42496  salexct  42498  salgenuni  42501  subsaliuncllem  42521  meadjiunlem  42628  caragenss  42667  caratheodory  42691  ovnlecvr  42721  ovnsslelem  42723  ovnlerp  42725  ovn0lem  42728  ovnsubaddlem1  42733  hoidmv1lelem1  42754  hoidmv1lelem3  42756  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvlelem4  42761  ovnhoilem1  42764  ovnhoilem2  42765  ovnlecvr2  42773  ovncvr2  42774  opnvonmbllem2  42796  ovolval4lem1  42812  ovolval5lem3  42817  pimconstlt1  42864  pimltpnf  42865  pimiooltgt  42870  pimgtmnf2  42873  pimdecfgtioc  42874  pimincfltioc  42875  pimdecfgtioo  42876  pimincfltioo  42877  sssmf  42896  incsmflem  42899  smfaddlem1  42920  smfaddlem2  42921  decsmflem  42923  smflimlem1  42928  smflimlem2  42929  smflimlem3  42930  smfrec  42945  smfmullem4  42950  smfdiv  42953  smfsuplem1  42966  smfsuplem3  42968  smfinflem  42972  smflimsuplem1  42975  smflimsuplem7  42981  smfliminflem  42985  sprsymrelfolem1  43501  prmdvdsfmtnof1lem1  43593  prmdvdsfmtnof  43595  perfectALTVlem2  43734  rabsubmgmd  43905  mgmhmeql  43917  oddibas  43927  2zlidl  44103  2zrngbas  44105  2zrng0  44107
  Copyright terms: Public domain W3C validator