Theorem ssrab2 3650

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 2905	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		ssab2 3649	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
3	1, 2	eqsstri 3598	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   ∧ wa 383   ∈ wcel 1977  {cab 2596  {crab 2900   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554

This theorem is referenced by:  ssrabeq  3651  iinrab2  4519  riinrab  4532  rabexg  4739  pwnss  4756  frminex  5018  wereu2  5035  dmmptss  5548  wfisg  5632  ssimaex  6173  f1oresrab  6302  weniso  6504  canth  6508  riotacl  6525  riotassuni  6547  onminesb  6890  onminsb  6891  onintrab  6893  onnminsb  6896  onminex  6899  tfis  6946  omsson  6961  suppssdm  7195  fnsuppres  7209  oawordeulem  7521  oeeulem  7568  nnawordex  7604  pmvalg  7755  fineqvlem  8059  ordtypelem2  8307  ordtypelem3  8308  ordtypelem4  8309  ordtypelem6  8311  hartogs  8332  wemapso2lem  8340  card2on  8342  wdom2d  8368  oemapvali  8464  wemapwe  8477  tz9.12lem1  8533  tz9.12lem3  8535  rankf  8540  cplem1  8635  cardf2  8652  cardid2  8662  cardmin2  8707  acni3  8753  dfac2a  8835  cofsmo  8974  coftr  8978  fin2i2  9023  isfin2-2  9024  enfin2i  9026  fin23lem28  9045  fin23lem30  9047  isf32lem5  9062  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  fin1a2lem11  9115  fin1a2lem12  9116  hsmexlem4  9134  hsmexlem5  9135  hsmexlem6  9136  axdc3lem4  9158  ac6num  9184  ac6  9185  zorn2lem1  9201  zorn2lem3  9203  zorn2lem4  9204  zorn2lem5  9205  ondomon  9264  alephval2  9273  pwfseqlem1  9359  pwfseqlem3  9361  wunccl  9445  tskmcl  9542  0nnq  9625  elpqn  9626  fiminre  10851  infm3  10861  uzf  11566  nnwos  11631  supminf  11651  zsupss  11653  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  rpre  11715  ixxf  12056  fzf  12201  flval3  12478  rabssnn0fi  12647  expge0  12758  expge1  12759  hashbclem  13093  sqrlem3  13833  sqrlem5  13835  rlimrege0  14158  incexc2  14409  dvdsflip  14877  divalglem2  14956  divalglem5  14958  divalglem8  14961  bitsf  14987  bitsfzolem  14994  sadadd2lem  15019  sadadd3  15021  sadcl  15022  smupf  15038  smuval2  15042  smupvallem  15043  smucl  15044  smueqlem  15050  gcdcllem3  15061  bezoutlem2  15095  bezoutlem3  15096  lcmcllem  15147  lcmn0cl  15148  lcmledvds  15150  lcmfval  15172  lcmfcllem  15176  lcmfn0cl  15177  lcmfledvds  15183  maxprmfct  15259  phicl2  15311  phibnd  15314  hashdvds  15318  phiprmpw  15319  phimullem  15322  eulerthlem2  15325  eulerth  15326  phisum  15333  odzcllem  15335  odzdvds  15338  pclem  15381  infpn2  15455  prmreclem1  15458  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  4sqlem13  15499  4sqlem14  15500  4sqlem17  15503  4sqlem18  15504  vdwnnlem3  15539  hashbccl  15545  ramcl2lem  15551  ramtcl  15552  ramtcl2  15553  ramtub  15554  prmgaplem3  15595  prmgaplem4  15596  prdsds  15947  imasdsval2  15999  mrcflem  16089  isacs1i  16141  wunnat  16439  dmcoass  16539  lublecl  16812  lubid  16813  gsumval1  17100  issubmd  17172  mhmeql  17187  nmzsubg  17458  nmznsg  17461  conjnmz  17517  conjnmzb  17518  gastacl  17565  cntzval  17577  cntzssv  17584  symgsssg  17710  symgfisg  17711  pmtrdifellem4  17722  odlem1  17777  odlem2  17781  odngen  17815  gexlem1  17817  gexlem2  17820  sylow1lem2  17837  sylow1lem3  17838  sylow1lem4  17839  sylow1lem5  17840  sylow2alem2  17856  sylow2a  17857  sylow2blem3  17860  sylow3lem2  17866  oddvdssubg  18081  cyggex2  18121  ablfacrplem  18287  ablfacrp2  18289  ablfac1eu  18295  pgpfaclem1  18303  ablfaclem2  18308  ablfaclem3  18309  lssacs  18788  lspf  18795  lspsolvlem  18963  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  rrgeq0  19111  rrgss  19113  asplss  19150  aspsubrg  19152  psrbagconf1o  19195  psrass1lem  19198  psrdi  19227  psrdir  19228  psrass23l  19229  psrass23  19231  resspsrmul  19238  mplbas  19250  mplbasss  19253  mplsubglem  19255  mplsubrglem  19260  mplmonmul  19285  psropprmul  19429  coe1mul2lem2  19459  cygznlem2a  19735  psgnghm  19745  ocvfval  19829  ocvval  19830  dsmmbase  19898  dsmmval2  19899  dsmmsubg  19906  frlmsslsp  19954  scmatlss  20150  smadiadet  20295  pmatcoe1fsupp  20325  cpmatsubgpmat  20344  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  clscld  20661  mretopd  20706  neips  20727  neiptopnei  20746  ordtbaslem  20802  ordtuni  20804  ordtcld1  20811  ordtcld2  20812  cnpfval  20848  iscnp2  20853  cmpcov2  21003  cmpsublem  21012  tgcmp  21014  hauscmplem  21019  concompcld  21047  1stcfb  21058  2ndc1stc  21064  2ndcdisj  21069  finlocfin  21133  kgentopon  21151  xkotf  21198  txkgen  21265  xkococnlem  21272  imastopn  21333  kqffn  21338  opnfbas  21456  flimfnfcls  21642  alexsubALT  21665  ptcmplem1  21666  ptcmplem2  21667  ptcmplem3  21668  symgtgp  21715  tgpconcompeqg  21725  tgpconcomp  21726  ghmcnp  21728  tsmsfbas  21741  eltsms  21746  utoptop  21848  utopbas  21849  imasdsf1olem  21988  blfvalps  21998  blfps  22021  blf  22022  blcld  22120  nmoffn  22325  nmofval  22328  nmogelb  22330  nmolb  22331  nmof  22333  icccmplem1  22433  icccmplem2  22434  icccmplem3  22435  ishtpy  22579  clsocv  22857  rrxnm  22987  rrxf  22992  minveclem3b  23007  minveclem4  23011  ivthlem1  23027  ivthlem2  23028  ivthlem3  23029  ovolcl  23053  ovollb  23054  ovolgelb  23055  ovolge0  23056  ovolsslem  23059  ovolshftlem1  23084  ovolshft  23086  ovolscalem1  23088  ovolscalem2  23089  ovolsca  23090  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicc2  23097  shftmbl  23113  iundisj  23123  dyadmax  23172  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  iblmbf  23340  mdegmullem  23642  uc1pval  23703  mon1pval  23705  elqaalem1  23878  elqaalem3  23880  aannenlem2  23888  aalioulem2  23892  radcnvcl  23975  radcnvlt1  23976  radcnvle  23978  abelthlem4  23992  abelthlem6  23994  abelthlem9  23998  abelth  23999  atancn  24463  lgamucov  24564  lgamucov2  24565  ftalem3  24601  ftalem4  24602  ftalem5  24603  efnnfsumcl  24629  isppw  24640  sgmval2  24669  efchtdvds  24685  sqff1o  24708  fsumdvdsdiaglem  24709  fsumdvdsdiag  24710  fsumdvdscom  24711  musum  24717  muinv  24719  dvdsmulf1o  24720  fsumdvdsmul  24721  sgmmul  24726  ppiub  24729  vmasum  24741  logfac2  24742  perfectlem2  24755  lgsfcl2  24828  lgsfcl  24830  lgscl  24836  lgsquadlem1  24905  lgsquadlem2  24906  rpvmasumlem  24976  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrisum0  25009  mudivsum  25019  mulogsum  25021  mulog2sumlem2  25024  vmalogdivsum2  25027  logsqvma  25031  logsqvma2  25032  selberglem3  25036  selberg  25037  selberg34r  25060  pntsval2  25065  pntrlog2bndlem1  25066  pntlem3  25098  tglnunirn  25243  tglnssp  25247  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  axcontlem10  25653  incistruhgr  25746  upgrss  25755  upgrn0  25756  upgruhgr  25768  umgrass  25848  umgran0  25849  umisuhgra  25856  usgrass  25890  uslisushgra  25892  usgrares1  25939  usgrafilem1  25940  nbgrassvt  25962  nbgraf1olem1  25970  cusgrares  26001  hashwwlkext  26274  clwwlksswrd  26305  vdgrun  26428  vdgrfiun  26429  konigsberg  26514  frisusgranb  26524  frgrawopreg1  26577  frgrawopreg2  26578  ocsh  27526  spancl  27579  shsval2i  27630  ococin  27651  chsupid  27655  speccl  28142  atssch  28586  hatomistici  28605  chpssati  28606  iundisjf  28784  aciunf1  28845  fcobijfs  28889  fpwrelmap  28896  iundisjfi  28942  locfinreflem  29235  esumrnmpt2  29457  esumpinfval  29462  sigagensiga  29531  ldgenpisyslem1  29553  ldgenpisys  29556  measvuni  29604  imambfm  29651  dya2iocuni  29672  omscl  29684  oms0  29686  omsmon  29687  omssubadd  29689  carsgcl  29693  oddpwdc  29743  eulerpartlem1  29756  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgs2  29769  ballotlem2  29877  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemfmpn  29883  ballotlemiex  29890  ballotlemsup  29893  ballotlem7  29924  ballotth  29926  bnj21  30037  bnj110  30182  bnj1204  30334  bnj1311  30346  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  erdszelem2  30428  conpcon  30471  cvmliftmolem2  30518  cvmliftlem15  30534  cvmlift2lem12  30550  snmlff  30565  tfisg  30960  frinsg  30986  wlimss  31022  sltval2  31053  nodenselem4  31083  nobndlem5  31095  nofulllem5  31105  rankeq1o  31448  finminlem  31482  fnessref  31522  neibastop1  31524  neibastop2lem  31525  bj-rabtr  32118  bj-rabtrALTALT  32120  bj-rabtrAUTO  32121  bj-cmnssmnd  32313  bj-vecssmod  32320  bj-rrvecssvec  32327  icoreresf  32376  phpreu  32563  fin2so  32566  poimirlem26  32605  poimirlem31  32610  poimirlem32  32611  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  ismblfin  32620  mbfposadd  32627  cnambfre  32628  cover2  32678  indexa  32698  fdc  32711  sstotbnd2  32743  sstotbnd3  32745  igenidl  33032  prnc  33036  toycom  33278  lkrlss  33400  atlatmstc  33624  atlatle  33625  glbconN  33681  linepsubN  34056  pmapssat  34063  pmaple  34065  pmapsub  34072  paddssat  34118  diass  35349  diaglbN  35362  diaintclN  35365  diassdvaN  35367  docaclN  35431  dibglbN  35473  dibintclN  35474  diclspsn  35501  dihglblem2N  35601  dih1dimatlem  35636  dihglb2  35649  dochval2  35659  dochcl  35660  dochvalr  35664  doch2val2  35671  dochss  35672  dochocss  35673  lclkr  35840  lclkrs  35846  lcdvbase  35900  lcdvbasess  35901  mapdunirnN  35957  mzpindd  36327  fiphp3d  36401  rencldnfilem  36402  irrapx1  36410  pellexlem3  36413  pellfundre  36463  pellfundge  36464  pellfundlb  36466  pellfundglb  36467  jm2.22  36580  jm2.23  36581  rpnnen3  36617  fglmod  36661  pwssplit4  36677  pwfi2f1o  36684  hbtlem6  36718  dgraalem  36734  dgraaub  36737  itgocn  36753  rgspncl  36758  rfovcnvf1od  37318  fsovfd  37326  fsovcnvlem  37327  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  uzwo4  38246  disjf1o  38373  icof  38406  fsumsupp0  38645  limcperiod  38695  sumnnodd  38697  fnlimabslt  38746  cncfshift  38759  cncfperiod  38764  ioodvbdlimc1lem1  38821  dvnprodlem1  38836  dvnprodlem2  38837  stoweidlem14  38907  stoweidlem34  38927  stoweidlem44  38937  stoweidlem50  38943  stoweidlem51  38944  stoweidlem52  38945  stoweidlem57  38950  stoweidlem59  38952  fourierdlem19  39019  fourierdlem20  39020  fourierdlem25  39025  fourierdlem31  39031  fourierdlem37  39037  fourierdlem42  39042  fourierdlem51  39050  fourierdlem54  39053  fourierdlem64  39063  fourierdlem79  39078  elaa2lem  39126  etransclem16  39143  etransclem24  39151  etransclem31  39158  etransclem33  39160  etransclem34  39161  etransclem48  39175  rrxbasefi  39179  salgencl  39226  salexct  39228  salgenuni  39231  subsaliuncllem  39251  meadjiunlem  39358  caragenss  39394  caratheodory  39418  ovnlecvr  39448  ovnsslelem  39450  ovnlerp  39452  ovn0lem  39455  ovnsubaddlem1  39460  hoidmv1lelem1  39481  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  ovnhoilem1  39491  ovnhoilem2  39492  ovnlecvr2  39500  ovncvr2  39501  opnvonmbllem2  39523  ovolval4lem1  39539  ovolval5lem3  39544  pimconstlt1  39592  pimltpnf  39593  pimiooltgt  39598  pimgtmnf2  39601  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  sssmf  39625  incsmflem  39628  smfaddlem1  39649  smfaddlem2  39650  decsmflem  39652  smflimlem1  39657  smflimlem2  39658  smflimlem3  39659  smfrec  39674  smfmullem4  39679  smfdiv  39682  prmdvdsfmtnof1lem1  40034  prmdvdsfmtnof  40036  perfectALTVlem2  40165  usgrss  40404  uspgrushgr  40405  ushgredgedga  40456  ushgredgedgaloop  40458  vtxdun  40696  hashwwlksnext  41120  clwwlkssswrd  41218  frcond3  41440  frgrwopreg1  41487  frgrwopreg2  41488  rabsubmgmd  41581  mgmhmeql  41593  oddibas  41603  2zlidl  41724  2zrngbas  41726  2zrng0  41728