Theorem ssrab2 3940

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

Syntax hints:   ∧ wa 387   ∈ wcel 2050  {cab 2752  {crab 3086   ⊆ wss 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-in 3830  df-ss 3837

This theorem is referenced by:  ssrab3  3941  ssrabeq  3943  iinrab2  4854  riinrab  4868  rabexg  5086  pwnss  5102  frminex  5383  wereu2  5400  wfisg  6018  ssimaex  6574  f1oresrab  6710  weniso  6928  canth  6932  riotacl  6949  riotassuni  6972  onminesb  7327  onminsb  7328  onintrab  7330  onnminsb  7333  onminex  7336  tfis  7383  suppssdm  7644  fnsuppres  7658  oeeulem  8026  nnawordex  8062  pmvalg  8215  fineqvlem  8525  ordtypelem3  8777  ordtypelem4  8778  ordtypelem6  8780  hartogs  8801  card2on  8811  wdom2d  8837  oemapvali  8939  tz9.12lem1  9008  tz9.12lem3  9010  rankf  9015  cardf2  9164  cardid2  9174  cardmin2  9219  acni3  9265  dfac2a  9347  cofsmo  9487  coftr  9491  fin2i2  9536  isfin2-2  9537  enfin2i  9539  fin1a2lem11  9628  fin1a2lem12  9629  axdc3lem4  9671  ac6num  9697  ac6  9698  ondomon  9781  alephval2  9790  pwfseqlem1  9876  pwfseqlem3  9878  wunccl  9962  tskmcl  10059  fiminreOLD  11389  infm3  11399  uzf  12059  nnwos  12127  supminf  12147  zsupss  12149  rpnnen1lem1  12190  rpnnen1lem3  12191  rpnnen1lem5  12193  rpreOLD  12211  ixxf  12562  fzf  12710  flval3  12998  rabssnn0fi  13167  expge0  13278  expge1  13279  hashbclem  13621  sqrlem3  14463  rlimrege0  14795  incexc2  15051  bitsf  15634  bitsfzolem  15641  sadadd2lem  15666  sadadd3  15668  sadcl  15669  smupf  15685  smuval2  15689  smupvallem  15690  smucl  15691  smueqlem  15697  lcmcllem  15794  lcmn0cl  15795  lcmledvds  15797  lcmfval  15819  lcmfcllem  15823  lcmfn0cl  15824  lcmfledvds  15830  phicl2  15959  phibnd  15962  hashdvds  15966  phiprmpw  15967  phimullem  15970  eulerth  15974  phisum  15981  odzcllem  15983  odzdvds  15986  prmreclem1  16106  prmreclem2  16107  prmreclem3  16108  prmreclem4  16109  prmreclem5  16110  hashbccl  16193  prmgaplem3  16243  prmgaplem4  16244  prdsds  16591  mrcflem  16747  isacs1i  16798  wunnat  17096  dmcoass  17196  lublecl  17469  lubid  17470  issubmd  17829  mhmeql  17844  cntzval  18234  cntzssv  18241  symgsssg  18368  symgfisg  18369  pmtrdifellem4  18380  odfval  18434  odlem1  18437  odlem2  18441  odngen  18475  gexlem1  18477  gexlem2  18480  sylow2alem2  18516  sylow2blem3  18520  oddvdssubg  18743  cyggex2  18783  ablfaclem3  18971  lssacs  19473  lspf  19480  asplss  19835  aspsubrg  19837  psrass1lem  19883  psrdi  19912  psrdir  19913  psrass23l  19914  psrass23  19916  resspsrmul  19923  mplbas  19935  mplsubglem  19940  mplsubrglem  19945  mplmonmul  19970  psropprmul  20121  ocvfval  20524  ocvval  20525  dsmmval2  20594  dsmmsubg  20601  scmatlss  20850  smadiadet  20995  pmatcoe1fsupp  21025  cpmatsubgpmat  21044  fctop  21328  cctop  21330  ppttop  21331  epttop  21333  clscld  21371  neips  21437  neiptopnei  21456  ordtbaslem  21512  ordtuni  21514  ordtcld1  21521  ordtcld2  21522  cnpfval  21558  iscnp2  21563  cmpcov2  21714  cmpsublem  21723  tgcmp  21725  conncompcld  21758  1stcfb  21769  2ndc1stc  21775  2ndcdisj  21780  finlocfin  21844  kgentopon  21862  xkotf  21909  txkgen  21976  xkococnlem  21983  imastopn  22044  kqffn  22049  opnfbas  22166  flimfnfcls  22352  alexsubALT  22375  ptcmplem2  22377  symgtgp  22425  tgpconncompeqg  22435  tgpconncomp  22436  ghmcnp  22438  tsmsfbas  22451  eltsms  22456  utoptop  22558  utopbas  22559  blfvalps  22708  blfps  22731  blf  22732  nmoffn  23035  nmofval  23038  nmogelb  23040  nmolb  23041  nmof  23043  ishtpy  23291  clsocv  23568  rrxnm  23709  rrxbasefi  23728  minveclem3b  23746  minveclem4  23750  ovolcl  23794  ovollb  23795  ovolgelb  23796  ovolge0  23797  ovolshftlem1  23825  ovolshft  23827  ovolscalem1  23829  ovolscalem2  23830  ovolsca  23831  ovolicc2lem3  23835  shftmbl  23854  iundisj  23864  dyadmax  23914  dyadmbllem  23915  opnmbllem  23917  mdegmullem  24387  uc1pval  24448  mon1pval  24450  elqaalem1  24623  elqaalem3  24625  aannenlem2  24633  aalioulem2  24637  radcnvcl  24720  radcnvlt1  24721  radcnvle  24723  ftalem4  25367  ftalem5  25368  efnnfsumcl  25394  isppw  25405  sgmval2  25434  efchtdvds  25450  sqff1o  25473  fsumdvdsdiaglem  25474  fsumdvdsdiag  25475  fsumdvdscom  25476  musum  25482  muinv  25484  sgmmul  25491  ppiub  25494  vmasum  25506  logfac2  25507  perfectlem2  25520  lgsfcl  25595  lgscl  25601  lgsquadlem1  25670  lgsquadlem2  25671  rpvmasumlem  25777  mudivsum  25820  mulogsum  25822  mulog2sumlem2  25825  vmalogdivsum2  25828  logsqvma  25832  logsqvma2  25833  selberglem3  25837  selberg  25838  selberg34r  25861  pntsval2  25866  pntrlog2bndlem1  25867  tglnunirn  26048  tglnssp  26052  incistruhgr  26579  upgrss  26588  upgrn0  26589  upgruhgr  26602  usgrss  26674  uspgrushgr  26675  ushgredgedg  26726  ushgredgedgloop  26728  vtxdun  26978  vtxdginducedm1  27040  wlknwwlksnbij  27387  hashwwlksnext  27431  hashwwlksnextOLD  27432  frcond3  27815  numclwlk1lem2  27935  ocsh  28853  spancl  28906  shsval2i  28957  ococin  28978  chsupid  28982  speccl  29469  hatomistici  29932  chpssati  29933  iundisjf  30119  aciunf1  30184  fcobijfs  30232  fpwrelmap  30242  iundisjfi  30289  locfinreflem  30777  esumrnmpt2  31000  esumpinfval  31005  sigagensiga  31074  ldgenpisyslem1  31096  ldgenpisys  31099  measvuni  31147  imambfm  31194  dya2iocuni  31215  omscl  31227  oms0  31229  omsmon  31230  omssubadd  31232  carsgcl  31236  oddpwdc  31286  eulerpartlem1  31299  eulerpartlemt  31303  eulerpartgbij  31304  eulerpartlemmf  31307  eulerpartlemgh  31310  eulerpartlemgs2  31312  ballotlem2  31421  ballotlemfc0  31425  ballotlemfcc  31426  ballotlemfmpn  31427  ballotlemiex  31434  ballotlemsup  31437  ballotlem7  31468  ballotth  31470  reprpmtf1o  31574  breprexplema  31578  hgt750lema  31605  bnj110  31806  bnj1204  31958  bnj1311  31970  subfacp1lem3  32043  subfacp1lem5  32045  subfacp1lem6  32046  erdszelem2  32053  connpconn  32096  cvmliftmolem2  32143  cvmliftlem15  32159  cvmlift2lem12  32175  snmlff  32190  tfisg  32605  frpomin  32628  frpoinsg  32631  frinsg  32637  sltval2  32713  conway  32814  scutun12  32821  scutbdaybnd  32825  scutbdaylt  32826  rankeq1o  33182  finminlem  33216  fnessref  33255  neibastop1  33257  neibastop2lem  33258  bj-rabtr  33772  bj-rabtrAUTO  33774  bj-cmnssmnd  34048  bj-vecssmod  34055  icoreresf  34104  phpreu  34346  fin2so  34349  poimirlem26  34388  poimirlem31  34393  poimirlem32  34394  opnmbllem0  34398  mblfinlem1  34399  mblfinlem2  34400  ismblfin  34403  mbfposadd  34409  cnambfre  34410  cover2  34460  indexa  34479  fdc  34491  sstotbnd2  34523  sstotbnd3  34525  igenidl  34812  prnc  34816  toycom  35583  lkrlss  35705  atlatmstc  35929  atlatle  35930  glbconN  35987  linepsubN  36362  pmapssat  36369  pmaple  36371  pmapsub  36378  paddssat  36424  diass  37652  diaglbN  37665  diaintclN  37668  diassdvaN  37670  docaclN  37734  dibglbN  37776  dibintclN  37777  diclspsn  37804  dihglblem2N  37904  dih1dimatlem  37939  dihglb2  37952  dochval2  37962  dochcl  37963  dochvalr  37967  doch2val2  37974  dochss  37975  dochocss  37976  lclkr  38143  lclkrs  38149  lcdvbase  38203  lcdvbasess  38204  mapdunirnN  38260  mzpindd  38767  fiphp3d  38841  rencldnfilem  38842  irrapx1  38850  pellexlem3  38853  pellfundre  38903  pellfundge  38904  pellfundlb  38906  pellfundglb  38907  jm2.22  39017  jm2.23  39018  rpnnen3  39054  pwssplit4  39114  pwfi2f1o  39121  hbtlem6  39154  dgraalem  39170  dgraaub  39173  itgocn  39189  rgspncl  39194  rfovcnvf1od  39742  fsovfd  39750  fsovcnvlem  39751  binomcxplemdvbinom  40130  binomcxplemcvg  40131  binomcxplemnotnn0  40133  uzwo4  40763  disjf1o  40902  icof  40933  allbutfiinf  41150  supminfxr  41196  supminfxr2  41201  fsumsupp0  41315  sumnnodd  41367  fnlimabslt  41416  liminfvalxr  41520  ioodvbdlimc1lem1  41671  dvnprodlem1  41686  dvnprodlem2  41687  stoweidlem14  41755  stoweidlem34  41775  stoweidlem44  41785  stoweidlem50  41791  stoweidlem51  41792  stoweidlem52  41793  stoweidlem57  41798  stoweidlem59  41800  fourierdlem19  41867  fourierdlem20  41868  fourierdlem25  41873  fourierdlem31  41879  fourierdlem37  41885  fourierdlem42  41890  fourierdlem51  41898  fourierdlem54  41901  fourierdlem64  41911  fourierdlem79  41926  elaa2lem  41974  etransclem16  41991  etransclem24  41999  etransclem31  42006  etransclem33  42008  etransclem34  42009  etransclem48  42023  salgencl  42071  salexct  42073  salgenuni  42076  subsaliuncllem  42096  meadjiunlem  42203  caragenss  42242  caratheodory  42266  ovnlecvr  42296  ovnsslelem  42298  ovnlerp  42300  ovn0lem  42303  ovnsubaddlem1  42308  hoidmv1lelem1  42329  hoidmv1lelem3  42331  hoidmvlelem1  42333  hoidmvlelem2  42334  hoidmvlelem3  42335  hoidmvlelem4  42336  ovnhoilem1  42339  ovnhoilem2  42340  ovnlecvr2  42348  ovncvr2  42349  opnvonmbllem2  42371  ovolval4lem1  42387  ovolval5lem3  42392  pimconstlt1  42439  pimltpnf  42440  pimiooltgt  42445  pimgtmnf2  42448  pimdecfgtioc  42449  pimincfltioc  42450  pimdecfgtioo  42451  pimincfltioo  42452  sssmf  42471  incsmflem  42474  smfaddlem1  42495  smfaddlem2  42496  decsmflem  42498  smflimlem1  42503  smflimlem2  42504  smflimlem3  42505  smfrec  42520  smfmullem4  42525  smfdiv  42528  smfsuplem1  42541  smfsuplem3  42543  smfinflem  42547  smflimsuplem1  42550  smflimsuplem7  42556  smfliminflem  42560  sprsymrelfolem1  43047  prmdvdsfmtnof1lem1  43139  prmdvdsfmtnof  43141  perfectALTVlem2  43280  rabsubmgmd  43451  mgmhmeql  43463  oddibas  43473  2zlidl  43594  2zrngbas  43596  2zrng0  43598