Theorem ssrab2 3979

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) (Proof shortened by BJ and SN, 8-Aug-2024.)

Assertion

Ref	Expression
ssrab2	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrabi 3585	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑦 ∈ 𝐴)
2	1	ssriv 3891	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:  {crab 3055   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  ssrab3  3981  ssrabeq  3983  iinrab2  4964  riinrab  4978  rabexg  5209  pwnss  5226  rabelpw  5229  frminex  5516  wereu2  5533  frpomin  6172  frpoinsg  6175  wfisg  6183  ssimaex  6774  f1oresrab  6920  weniso  7141  canth  7145  riotacl  7166  riotassuni  7189  onminesb  7555  onminsb  7556  onintrab  7558  onnminsb  7561  onminex  7564  tfis  7611  suppssdm  7897  fnsuppres  7911  oeeulem  8307  nnawordex  8343  pmvalg  8497  fineqvlem  8868  ordtypelem3  9114  ordtypelem4  9115  ordtypelem6  9117  hartogs  9138  card2on  9148  wdom2d  9174  oemapvali  9277  tz9.12lem1  9368  tz9.12lem3  9370  rankf  9375  cardf2  9524  cardid2  9534  cardmin2  9580  acni3  9626  dfac2a  9708  cofsmo  9848  coftr  9852  fin2i2  9897  isfin2-2  9898  enfin2i  9900  fin1a2lem11  9989  fin1a2lem12  9990  axdc3lem4  10032  ac6  10059  ondomon  10142  alephval2  10151  pwfseqlem1  10237  pwfseqlem3  10239  wunccl  10323  tskmcl  10420  infm3  11756  uzf  12406  nnwos  12476  supminf  12496  zsupss  12498  rpnnen1lem1  12539  rpnnen1lem3  12540  rpnnen1lem5  12542  ixxf  12910  fzf  13064  flval3  13355  rabssnn0fi  13524  expge0  13636  expge1  13637  hashbclem  13981  sqrlem3  14773  rlimrege0  15105  incexc2  15365  bitsf  15949  bitsfzolem  15956  sadadd2lem  15981  sadadd3  15983  sadcl  15984  smupf  16000  smuval2  16004  smupvallem  16005  smucl  16006  smueqlem  16012  lcmcllem  16116  lcmn0cl  16117  lcmledvds  16119  lcmfval  16141  lcmfcllem  16145  lcmfn0cl  16146  lcmfledvds  16152  phicl2  16284  phibnd  16287  hashdvds  16291  phiprmpw  16292  phimullem  16295  eulerth  16299  phisum  16306  odzcllem  16308  odzdvds  16311  prmreclem1  16432  prmreclem2  16433  prmreclem3  16434  prmreclem4  16435  prmreclem5  16436  hashbccl  16519  prmgaplem3  16569  prmgaplem4  16570  prdsds  16923  mrcflem  17063  isacs1i  17114  wunnat  17417  wunnatOLD  17418  dmcoass  17526  lublecl  17821  lubid  17822  issubmd  18187  mhmeql  18206  cntzval  18669  cntzssv  18676  symgsssg  18813  symgfisg  18814  pmtrdifellem4  18825  odfval  18878  odlem1  18881  odlem2  18885  odngen  18920  gexlem1  18922  gexlem2  18925  sylow2alem2  18961  sylow2blem3  18965  oddvdssubg  19194  cyggex2  19236  ablfaclem3  19428  lssacs  19958  lspf  19965  ocvfval  20582  ocvval  20583  dsmmval2  20652  dsmmsubg  20659  asplss  20787  aspsubrg  20789  psrass1lemOLD  20853  psrass1lem  20856  psrdi  20885  psrdir  20886  psrass23l  20887  psrass23  20889  resspsrmul  20896  mplbas  20908  mplsubglem  20915  mplsubrglem  20920  mplmonmul  20947  psropprmul  21113  scmatlss  21376  smadiadet  21521  pmatcoe1fsupp  21552  cpmatsubgpmat  21571  fctop  21855  cctop  21857  ppttop  21858  epttop  21860  clscld  21898  neips  21964  neiptopnei  21983  ordtbaslem  22039  ordtuni  22041  ordtcld1  22048  ordtcld2  22049  cnpfval  22085  iscnp2  22090  cmpcov2  22241  cmpsublem  22250  tgcmp  22252  conncompcld  22285  1stcfb  22296  2ndc1stc  22302  2ndcdisj  22307  finlocfin  22371  kgentopon  22389  xkotf  22436  txkgen  22503  xkococnlem  22510  imastopn  22571  kqffn  22576  opnfbas  22693  flimfnfcls  22879  alexsubALT  22902  ptcmplem2  22904  symgtgp  22957  tgpconncompeqg  22963  tgpconncomp  22964  ghmcnp  22966  tsmsfbas  22979  eltsms  22984  utoptop  23086  utopbas  23087  blfvalps  23235  blfps  23258  blf  23259  nmoffn  23563  nmofval  23566  nmogelb  23568  nmolb  23569  nmof  23571  ishtpy  23823  clsocv  24101  rrxnm  24242  rrxbasefi  24261  minveclem3b  24279  minveclem4  24283  ovolcl  24329  ovollb  24330  ovolgelb  24331  ovolge0  24332  ovolshftlem1  24360  ovolshft  24362  ovolscalem1  24364  ovolscalem2  24365  ovolsca  24366  ovolicc2lem3  24370  shftmbl  24389  iundisj  24399  dyadmax  24449  dyadmbllem  24450  opnmbllem  24452  mdegmullem  24930  uc1pval  24991  mon1pval  24993  elqaalem1  25166  elqaalem3  25168  aannenlem2  25176  aalioulem2  25180  radcnvcl  25263  radcnvlt1  25264  radcnvle  25266  ftalem4  25912  ftalem5  25913  efnnfsumcl  25939  isppw  25950  sgmval2  25979  efchtdvds  25995  sqff1o  26018  fsumdvdsdiaglem  26019  fsumdvdsdiag  26020  fsumdvdscom  26021  musum  26027  muinv  26029  sgmmul  26036  ppiub  26039  vmasum  26051  logfac2  26052  perfectlem2  26065  lgsfcl  26140  lgscl  26146  lgsquadlem1  26215  lgsquadlem2  26216  rpvmasumlem  26322  mudivsum  26365  mulogsum  26367  mulog2sumlem2  26370  vmalogdivsum2  26373  logsqvma  26377  logsqvma2  26378  selberglem3  26382  selberg  26383  selberg34r  26406  pntsval2  26411  pntrlog2bndlem1  26412  tglnunirn  26593  tglnssp  26597  incistruhgr  27124  upgrss  27133  upgrn0  27134  upgruhgr  27147  usgrss  27219  uspgrushgr  27220  ushgredgedg  27271  ushgredgedgloop  27273  vtxdun  27523  vtxdginducedm1  27585  wlknwwlksnbij  27926  hashwwlksnext  27952  frcond3  28306  numclwlk1lem2  28407  ocsh  29318  spancl  29371  shsval2i  29422  ococin  29443  chsupid  29447  speccl  29934  hatomistici  30397  chpssati  30398  iundisjf  30601  aciunf1  30674  fpwrelmap  30742  iundisjfi  30791  pwrssmgc  30951  cycpmco2f1  31064  cycpmco2rn  31065  cycpmco2lem1  31066  cycpmco2lem2  31067  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2lem7  31072  cycpmco2  31073  nsgmgclem  31264  locfinreflem  31458  zarclsiin  31489  zarcls  31492  zartopn  31493  esumrnmpt2  31702  esumpinfval  31707  sigagensiga  31775  ldgenpisyslem1  31797  ldgenpisys  31800  measvuni  31848  imambfm  31895  dya2iocuni  31916  omscl  31928  oms0  31930  omsmon  31931  omssubadd  31933  carsgcl  31937  oddpwdc  31987  eulerpartlem1  32000  eulerpartlemt  32004  eulerpartgbij  32005  eulerpartlemmf  32008  eulerpartlemgh  32011  eulerpartlemgs2  32013  ballotlem2  32121  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemfmpn  32127  ballotlemiex  32134  ballotlemsup  32137  ballotlem7  32168  ballotth  32170  reprpmtf1o  32272  breprexplema  32276  hgt750lema  32303  bnj110  32505  bnj1204  32659  bnj1311  32671  fnrelpredd  32728  subfacp1lem6  32814  erdszelem2  32821  connpconn  32864  cvmliftmolem2  32911  cvmliftlem15  32927  cvmlift2lem12  32943  snmlff  32958  satfrnmapom  32999  tfisg  33456  frinsg  33462  sltval2  33545  conway  33679  eqscut2  33686  scutun12  33690  scutbdaybnd  33695  scutbdaybnd2  33696  scutbdaylt  33698  bday1s  33711  madef  33726  leftssold  33747  rightssold  33748  madebdaylemlrcut  33765  cofcut1  33776  cofcutr  33778  rankeq1o  34159  finminlem  34193  fnessref  34232  neibastop1  34234  neibastop2lem  34235  bj-rabtr  34804  bj-rabtrAUTO  34806  bj-vecssmod  35136  icoreresf  35209  phpreu  35447  fin2so  35450  poimirlem26  35489  poimirlem31  35494  poimirlem32  35495  opnmbllem0  35499  mblfinlem1  35500  mblfinlem2  35501  ismblfin  35504  mbfposadd  35510  cnambfre  35511  cover2  35558  indexa  35577  fdc  35589  sstotbnd2  35618  sstotbnd3  35620  igenidl  35907  prnc  35911  toycom  36673  lkrlss  36795  atlatmstc  37019  atlatle  37020  glbconN  37077  linepsubN  37452  pmapssat  37459  pmaple  37461  pmapsub  37468  paddssat  37514  diass  38742  diaglbN  38755  diaintclN  38758  diassdvaN  38760  docaclN  38824  dibglbN  38866  dibintclN  38867  diclspsn  38894  dihglblem2N  38994  dih1dimatlem  39029  dihglb2  39042  dochval2  39052  dochcl  39053  dochvalr  39057  doch2val2  39064  dochss  39065  dochocss  39066  lclkr  39233  lclkrs  39239  lcdvbase  39293  lcdvbasess  39294  mapdunirnN  39350  sticksstones1  39771  mhpind  39934  infdesc  40124  mzpindd  40212  fiphp3d  40285  rencldnfilem  40286  irrapx1  40294  pellexlem3  40297  pellfundre  40347  pellfundge  40348  pellfundlb  40350  pellfundglb  40351  jm2.22  40461  jm2.23  40462  rpnnen3  40498  pwssplit4  40558  pwfi2f1o  40565  hbtlem6  40598  dgraalem  40614  dgraaub  40617  itgocn  40633  rgspncl  40638  rfovcnvf1od  41230  fsovfd  41238  fsovcnvlem  41239  binomcxplemdvbinom  41585  binomcxplemcvg  41586  binomcxplemnotnn0  41588  uzwo4  42215  disjf1o  42343  icof  42373  allbutfiinf  42574  supminfxr  42620  supminfxr2  42625  fsumsupp0  42737  sumnnodd  42789  fnlimabslt  42838  liminfvalxr  42942  ioodvbdlimc1lem1  43090  dvnprodlem1  43105  dvnprodlem2  43106  stoweidlem14  43173  stoweidlem34  43193  stoweidlem44  43203  stoweidlem50  43209  stoweidlem51  43210  stoweidlem52  43211  stoweidlem57  43216  stoweidlem59  43218  fourierdlem19  43285  fourierdlem20  43286  fourierdlem25  43291  fourierdlem31  43297  fourierdlem37  43303  fourierdlem42  43308  fourierdlem51  43316  fourierdlem54  43319  fourierdlem64  43329  fourierdlem79  43344  elaa2lem  43392  etransclem16  43409  etransclem24  43417  etransclem31  43424  etransclem33  43426  etransclem34  43427  etransclem48  43441  salgencl  43489  salexct  43491  salgenuni  43494  subsaliuncllem  43514  meadjiunlem  43621  caragenss  43660  caratheodory  43684  ovnlecvr  43714  ovnsslelem  43716  ovnlerp  43718  ovn0lem  43721  ovnsubaddlem1  43726  hoidmv1lelem1  43747  hoidmv1lelem3  43749  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  ovnhoilem1  43757  ovnhoilem2  43758  ovnlecvr2  43766  ovncvr2  43767  opnvonmbllem2  43789  ovolval4lem1  43805  ovolval5lem3  43810  pimconstlt1  43857  pimltpnf  43858  pimiooltgt  43863  pimgtmnf2  43866  pimdecfgtioc  43867  pimincfltioc  43868  pimdecfgtioo  43869  pimincfltioo  43870  sssmf  43889  incsmflem  43892  smfaddlem1  43913  smfaddlem2  43914  decsmflem  43916  smflimlem1  43921  smflimlem2  43922  smflimlem3  43923  smfrec  43938  smfmullem4  43943  smfdiv  43946  smfsuplem1  43959  smfsuplem3  43961  smfinflem  43965  smflimsuplem1  43968  smflimsuplem7  43974  smfliminflem  43978  sprsymrelfolem1  44560  prmdvdsfmtnof1lem1  44652  prmdvdsfmtnof  44654  perfectALTVlem2  44790  rabsubmgmd  44961  mgmhmeql  44973  oddibas  44983  2zlidl  45108  2zrngbas  45110  2zrng0  45112  isclatd  45885  topclat  45900