Theorem ssrab2 3687

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

Step	Hyp	Ref	Expression
1		df-rab 2921	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		ssab2 3686	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
3	1, 2	eqsstri 3635	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   ∧ wa 384   ∈ wcel 1990  {cab 2608  {crab 2916   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588

This theorem is referenced by:  ssrab3  3688  ssrabeq  3689  iinrab2  4583  riinrab  4596  rabexg  4812  pwnss  4830  frminex  5094  wereu2  5111  dmmptss  5631  wfisg  5715  ssimaex  6263  f1oresrab  6395  weniso  6604  canth  6608  riotacl  6625  riotassuni  6648  onminesb  6998  onminsb  6999  onintrab  7001  onnminsb  7004  onminex  7007  tfis  7054  omsson  7069  suppssdm  7308  fnsuppres  7322  oawordeulem  7634  oeeulem  7681  nnawordex  7717  pmvalg  7868  fineqvlem  8174  ordtypelem2  8424  ordtypelem3  8425  ordtypelem4  8426  ordtypelem6  8428  hartogs  8449  wemapso2lem  8457  card2on  8459  wdom2d  8485  oemapvali  8581  wemapwe  8594  tz9.12lem1  8650  tz9.12lem3  8652  rankf  8657  cplem1  8752  cardf2  8769  cardid2  8779  cardmin2  8824  acni3  8870  dfac2a  8952  cofsmo  9091  coftr  9095  fin2i2  9140  isfin2-2  9141  enfin2i  9143  fin23lem28  9162  fin23lem30  9164  isf32lem5  9179  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  fin1a2lem11  9232  fin1a2lem12  9233  hsmexlem4  9251  hsmexlem5  9252  hsmexlem6  9253  axdc3lem4  9275  ac6num  9301  ac6  9302  zorn2lem1  9318  zorn2lem3  9320  zorn2lem4  9321  zorn2lem5  9322  ondomon  9385  alephval2  9394  pwfseqlem1  9480  pwfseqlem3  9482  wunccl  9566  tskmcl  9663  0nnq  9746  elpqn  9747  fiminre  10972  infm3  10982  uzf  11690  nnwos  11755  supminf  11775  zsupss  11777  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  rpre  11839  ixxf  12185  fzf  12330  flval3  12616  rabssnn0fi  12785  expge0  12896  expge1  12897  hashbclem  13236  sqrlem3  13985  sqrlem5  13987  rlimrege0  14310  incexc2  14570  dvdsflip  15039  divalglem2  15118  divalglem5  15120  divalglem8  15123  bitsf  15149  bitsfzolem  15156  sadadd2lem  15181  sadadd3  15183  sadcl  15184  smupf  15200  smuval2  15204  smupvallem  15205  smucl  15206  smueqlem  15212  gcdcllem3  15223  bezoutlem2  15257  bezoutlem3  15258  lcmcllem  15309  lcmn0cl  15310  lcmledvds  15312  lcmfval  15334  lcmfcllem  15338  lcmfn0cl  15339  lcmfledvds  15345  maxprmfct  15421  phicl2  15473  phibnd  15476  hashdvds  15480  phiprmpw  15481  phimullem  15484  eulerthlem2  15487  eulerth  15488  phisum  15495  odzcllem  15497  odzdvds  15500  pclem  15543  infpn2  15617  prmreclem1  15620  prmreclem2  15621  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  4sqlem13  15661  4sqlem14  15662  4sqlem17  15665  4sqlem18  15666  vdwnnlem3  15701  hashbccl  15707  ramcl2lem  15713  ramtcl  15714  ramtcl2  15715  ramtub  15716  prmgaplem3  15757  prmgaplem4  15758  prdsds  16124  imasdsval2  16176  mrcflem  16266  isacs1i  16318  wunnat  16616  dmcoass  16716  lublecl  16989  lubid  16990  gsumval1  17277  issubmd  17349  mhmeql  17364  nmzsubg  17635  nmznsg  17638  conjnmz  17694  conjnmzb  17695  gastacl  17742  cntzval  17754  cntzssv  17761  symgsssg  17887  symgfisg  17888  pmtrdifellem4  17899  odlem1  17954  odlem2  17958  odngen  17992  gexlem1  17994  gexlem2  17997  sylow1lem2  18014  sylow1lem3  18015  sylow1lem4  18016  sylow1lem5  18017  sylow2alem2  18033  sylow2a  18034  sylow2blem3  18037  sylow3lem2  18043  oddvdssubg  18258  cyggex2  18298  ablfacrplem  18464  ablfacrp2  18466  ablfac1eu  18472  pgpfaclem1  18480  ablfaclem2  18485  ablfaclem3  18486  lssacs  18967  lspf  18974  lspsolvlem  19142  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  rrgeq0  19290  rrgss  19292  asplss  19329  aspsubrg  19331  psrbagconf1o  19374  psrass1lem  19377  psrdi  19406  psrdir  19407  psrass23l  19408  psrass23  19410  resspsrmul  19417  mplbas  19429  mplbasss  19432  mplsubglem  19434  mplsubrglem  19439  mplmonmul  19464  psropprmul  19608  coe1mul2lem2  19638  cygznlem2a  19916  psgnghm  19926  ocvfval  20010  ocvval  20011  dsmmbase  20079  dsmmval2  20080  dsmmsubg  20087  frlmsslsp  20135  scmatlss  20331  smadiadet  20476  pmatcoe1fsupp  20506  cpmatsubgpmat  20525  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  clscld  20851  mretopd  20896  neips  20917  neiptopnei  20936  ordtbaslem  20992  ordtuni  20994  ordtcld1  21001  ordtcld2  21002  cnpfval  21038  iscnp2  21043  cmpcov2  21193  cmpsublem  21202  tgcmp  21204  hauscmplem  21209  conncompcld  21237  1stcfb  21248  2ndc1stc  21254  2ndcdisj  21259  finlocfin  21323  kgentopon  21341  xkotf  21388  txkgen  21455  xkococnlem  21462  imastopn  21523  kqffn  21528  opnfbas  21646  flimfnfcls  21832  alexsubALT  21855  ptcmplem1  21856  ptcmplem2  21857  ptcmplem3  21858  symgtgp  21905  tgpconncompeqg  21915  tgpconncomp  21916  ghmcnp  21918  tsmsfbas  21931  eltsms  21936  utoptop  22038  utopbas  22039  imasdsf1olem  22178  blfvalps  22188  blfps  22211  blf  22212  blcld  22310  nmoffn  22515  nmofval  22518  nmogelb  22520  nmolb  22521  nmof  22523  icccmplem1  22625  icccmplem2  22626  icccmplem3  22627  ishtpy  22771  clsocv  23049  rrxnm  23179  rrxf  23184  minveclem3b  23199  minveclem4  23203  ivthlem1  23220  ivthlem2  23221  ivthlem3  23222  ovolcl  23246  ovollb  23247  ovolgelb  23248  ovolge0  23249  ovolsslem  23252  ovolshftlem1  23277  ovolshft  23279  ovolscalem1  23281  ovolscalem2  23282  ovolsca  23283  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicc2  23290  shftmbl  23306  iundisj  23316  dyadmax  23366  dyadmbllem  23367  dyadmbl  23368  opnmbllem  23369  iblmbf  23534  mdegmullem  23838  uc1pval  23899  mon1pval  23901  elqaalem1  24074  elqaalem3  24076  aannenlem2  24084  aalioulem2  24088  radcnvcl  24171  radcnvlt1  24172  radcnvle  24174  abelthlem4  24188  abelthlem6  24190  abelthlem9  24194  abelth  24195  atancn  24663  lgamucov  24764  lgamucov2  24765  ftalem3  24801  ftalem4  24802  ftalem5  24803  efnnfsumcl  24829  isppw  24840  sgmval2  24869  efchtdvds  24885  sqff1o  24908  fsumdvdsdiaglem  24909  fsumdvdsdiag  24910  fsumdvdscom  24911  musum  24917  muinv  24919  dvdsmulf1o  24920  fsumdvdsmul  24921  sgmmul  24926  ppiub  24929  vmasum  24941  logfac2  24942  perfectlem2  24955  lgsfcl2  25028  lgsfcl  25030  lgscl  25036  lgsquadlem1  25105  lgsquadlem2  25106  rpvmasumlem  25176  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  mudivsum  25219  mulogsum  25221  mulog2sumlem2  25224  vmalogdivsum2  25227  logsqvma  25231  logsqvma2  25232  selberglem3  25236  selberg  25237  selberg34r  25260  pntsval2  25265  pntrlog2bndlem1  25266  pntlem3  25298  tglnunirn  25443  tglnssp  25447  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  axcontlem10  25853  incistruhgr  25974  upgrss  25983  upgrn0  25984  upgruhgr  25997  usgrss  26069  uspgrushgr  26070  ushgredgedg  26121  ushgredgedgloop  26123  upgrreslem  26196  umgrreslem  26197  vtxdun  26377  vtxdginducedm1lem2  26436  vtxdginducedm1  26439  finsumvtxdg2ssteplem1  26441  hashwwlksnext  26809  clwwlkssswrd  26911  frcond3  27133  ocsh  28142  spancl  28195  shsval2i  28246  ococin  28267  chsupid  28271  speccl  28758  atssch  29202  hatomistici  29221  chpssati  29222  iundisjf  29402  aciunf1  29463  fcobijfs  29501  fpwrelmap  29508  iundisjfi  29555  locfinreflem  29907  esumrnmpt2  30130  esumpinfval  30135  sigagensiga  30204  ldgenpisyslem1  30226  ldgenpisys  30229  measvuni  30277  imambfm  30324  dya2iocuni  30345  omscl  30357  oms0  30359  omsmon  30360  omssubadd  30362  carsgcl  30366  oddpwdc  30416  eulerpartlem1  30429  eulerpartlemt  30433  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpartlemgh  30440  eulerpartlemgs2  30442  ballotlem2  30550  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemfmpn  30556  ballotlemiex  30563  ballotlemsup  30566  ballotlem7  30597  ballotth  30599  reprpmtf1o  30704  breprexplema  30708  hgt750lema  30735  bnj110  30928  bnj1204  31080  bnj1311  31092  subfacp1lem3  31164  subfacp1lem5  31166  subfacp1lem6  31167  erdszelem2  31174  connpconn  31217  cvmliftmolem2  31264  cvmliftlem15  31280  cvmlift2lem12  31296  snmlff  31311  tfisg  31716  frinsg  31742  wlimss  31778  sltval2  31809  conway  31910  scutun12  31917  scutbdaybnd  31921  scutbdaylt  31922  rankeq1o  32278  finminlem  32312  fnessref  32352  neibastop1  32354  neibastop2lem  32355  bj-rabtr  32926  bj-rabtrALTALT  32928  bj-rabtrAUTO  32929  bj-cmnssmnd  33136  bj-vecssmod  33143  bj-rrvecssvec  33150  icoreresf  33200  phpreu  33393  fin2so  33396  poimirlem26  33435  poimirlem31  33440  poimirlem32  33441  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  ismblfin  33450  mbfposadd  33457  cnambfre  33458  cover2  33508  indexa  33528  fdc  33541  sstotbnd2  33573  sstotbnd3  33575  igenidl  33862  prnc  33866  toycom  34260  lkrlss  34382  atlatmstc  34606  atlatle  34607  glbconN  34663  linepsubN  35038  pmapssat  35045  pmaple  35047  pmapsub  35054  paddssat  35100  diass  36331  diaglbN  36344  diaintclN  36347  diassdvaN  36349  docaclN  36413  dibglbN  36455  dibintclN  36456  diclspsn  36483  dihglblem2N  36583  dih1dimatlem  36618  dihglb2  36631  dochval2  36641  dochcl  36642  dochvalr  36646  doch2val2  36653  dochss  36654  dochocss  36655  lclkr  36822  lclkrs  36828  lcdvbase  36882  lcdvbasess  36883  mapdunirnN  36939  mzpindd  37309  fiphp3d  37383  rencldnfilem  37384  irrapx1  37392  pellexlem3  37395  pellfundre  37445  pellfundge  37446  pellfundlb  37448  pellfundglb  37449  jm2.22  37562  jm2.23  37563  rpnnen3  37599  fglmod  37643  pwssplit4  37659  pwfi2f1o  37666  hbtlem6  37699  dgraalem  37715  dgraaub  37718  itgocn  37734  rgspncl  37739  rfovcnvf1od  38298  fsovfd  38306  fsovcnvlem  38307  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  uzwo4  39221  disjf1o  39378  icof  39411  allbutfiinf  39647  supminfxr  39694  supminfxr2  39699  fsumsupp0  39810  limcperiod  39860  sumnnodd  39862  fnlimabslt  39911  liminfvalxr  40015  cncfshift  40087  cncfperiod  40092  ioodvbdlimc1lem1  40146  dvnprodlem1  40161  dvnprodlem2  40162  stoweidlem14  40231  stoweidlem34  40251  stoweidlem44  40261  stoweidlem50  40267  stoweidlem51  40268  stoweidlem52  40269  stoweidlem57  40274  stoweidlem59  40276  fourierdlem19  40343  fourierdlem20  40344  fourierdlem25  40349  fourierdlem31  40355  fourierdlem37  40361  fourierdlem42  40366  fourierdlem51  40374  fourierdlem54  40377  fourierdlem64  40387  fourierdlem79  40402  elaa2lem  40450  etransclem16  40467  etransclem24  40475  etransclem31  40482  etransclem33  40484  etransclem34  40485  etransclem48  40499  rrxbasefi  40503  salgencl  40550  salexct  40552  salgenuni  40555  subsaliuncllem  40575  meadjiunlem  40682  caragenss  40718  caratheodory  40742  ovnlecvr  40772  ovnsslelem  40774  ovnlerp  40776  ovn0lem  40779  ovnsubaddlem1  40784  hoidmv1lelem1  40805  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  ovnhoilem1  40815  ovnhoilem2  40816  ovnlecvr2  40824  ovncvr2  40825  opnvonmbllem2  40847  ovolval4lem1  40863  ovolval5lem3  40868  pimconstlt1  40915  pimltpnf  40916  pimiooltgt  40921  pimgtmnf2  40924  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  sssmf  40947  incsmflem  40950  smfaddlem1  40971  smfaddlem2  40972  decsmflem  40974  smflimlem1  40979  smflimlem2  40980  smflimlem3  40981  smfrec  40996  smfmullem4  41001  smfdiv  41004  smfsuplem1  41017  smfsuplem3  41019  smfinflem  41023  smflimsuplem1  41026  smflimsuplem7  41032  smfliminflem  41036  prmdvdsfmtnof1lem1  41496  prmdvdsfmtnof  41498  perfectALTVlem2  41631  sprsymrelfolem1  41742  rabsubmgmd  41791  mgmhmeql  41803  oddibas  41813  2zlidl  41934  2zrngbas  41936  2zrng0  41938