Theorem ssrab2 4014

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 3619	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑦 ∈ 𝐴)
2	1	ssriv 3926	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:  {crab 3069   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  ssrab3  4016  ssrabeq  4018  iinrab2  5000  riinrab  5014  rabexg  5256  pwnss  5273  rabelpw  5276  frminex  5570  wereu2  5587  predres  6246  frpomin  6247  frpoinsg  6250  wfisgOLD  6261  ssimaex  6862  f1oresrab  7008  weniso  7234  canth  7238  riotacl  7259  riotassuni  7282  onminesb  7652  onminsb  7653  onintrab  7655  onnminsb  7658  onminex  7661  tfis  7710  suppssdm  8002  fnsuppres  8016  oeeulem  8441  nnawordex  8477  pmvalg  8635  fineqvlem  9046  ordtypelem3  9288  ordtypelem4  9289  ordtypelem6  9291  hartogs  9312  card2on  9322  wdom2d  9348  oemapvali  9451  frinsg  9518  tz9.12lem1  9554  tz9.12lem3  9556  rankf  9561  cardf2  9710  cardid2  9720  cardmin2  9766  acni3  9812  dfac2a  9894  cofsmo  10034  coftr  10038  fin2i2  10083  isfin2-2  10084  enfin2i  10086  fin1a2lem11  10175  fin1a2lem12  10176  axdc3lem4  10218  ac6  10245  ondomon  10328  alephval2  10337  pwfseqlem1  10423  pwfseqlem3  10425  wunccl  10509  tskmcl  10606  infm3  11943  uzf  12594  nnwos  12664  supminf  12684  zsupss  12686  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  ixxf  13098  fzf  13252  flval3  13544  rabssnn0fi  13715  expge0  13828  expge1  13829  hashbclem  14173  sqrlem3  14965  rlimrege0  15297  incexc2  15559  bitsf  16143  bitsfzolem  16150  sadadd2lem  16175  sadadd3  16177  sadcl  16178  smupf  16194  smuval2  16198  smupvallem  16199  smucl  16200  smueqlem  16206  lcmcllem  16310  lcmn0cl  16311  lcmledvds  16313  lcmfval  16335  lcmfcllem  16339  lcmfn0cl  16340  lcmfledvds  16346  phicl2  16478  phibnd  16481  hashdvds  16485  phiprmpw  16486  phimullem  16489  eulerth  16493  phisum  16500  odzcllem  16502  odzdvds  16505  prmreclem1  16626  prmreclem2  16627  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  hashbccl  16713  prmgaplem3  16763  prmgaplem4  16764  prdsds  17184  mrcflem  17324  isacs1i  17375  wunnat  17681  wunnatOLD  17682  dmcoass  17790  lublecl  18088  lubid  18089  issubmd  18454  mhmeql  18473  cntzval  18936  cntzssv  18943  symgsssg  19084  symgfisg  19085  pmtrdifellem4  19096  odfval  19149  odlem1  19152  odlem2  19156  odngen  19191  gexlem1  19193  gexlem2  19196  sylow2alem2  19232  sylow2blem3  19236  oddvdssubg  19465  cyggex2  19507  ablfaclem3  19699  lssacs  20238  lspf  20245  ocvfval  20880  ocvval  20881  dsmmval2  20952  dsmmsubg  20959  asplss  21087  aspsubrg  21089  psrass1lemOLD  21152  psrass1lem  21155  psrdi  21184  psrdir  21185  psrass23l  21186  psrass23  21188  resspsrmul  21195  mplbas  21207  mplsubglem  21214  mplsubrglem  21219  mplmonmul  21246  psropprmul  21418  scmatlss  21683  smadiadet  21828  pmatcoe1fsupp  21859  cpmatsubgpmat  21878  fctop  22163  cctop  22165  ppttop  22166  epttop  22168  clscld  22207  neips  22273  neiptopnei  22292  ordtbaslem  22348  ordtuni  22350  ordtcld1  22357  ordtcld2  22358  cnpfval  22394  iscnp2  22399  cmpcov2  22550  cmpsublem  22559  tgcmp  22561  conncompcld  22594  1stcfb  22605  2ndc1stc  22611  2ndcdisj  22616  finlocfin  22680  kgentopon  22698  xkotf  22745  txkgen  22812  xkococnlem  22819  imastopn  22880  kqffn  22885  opnfbas  23002  flimfnfcls  23188  alexsubALT  23211  ptcmplem2  23213  symgtgp  23266  tgpconncompeqg  23272  tgpconncomp  23273  ghmcnp  23275  tsmsfbas  23288  eltsms  23293  utoptop  23395  utopbas  23396  blfvalps  23545  blfps  23568  blf  23569  nmoffn  23884  nmofval  23887  nmogelb  23889  nmolb  23890  nmof  23892  ishtpy  24144  clsocv  24423  rrxnm  24564  rrxbasefi  24583  minveclem3b  24601  minveclem4  24605  ovolcl  24651  ovollb  24652  ovolgelb  24653  ovolge0  24654  ovolshftlem1  24682  ovolshft  24684  ovolscalem1  24686  ovolscalem2  24687  ovolsca  24688  ovolicc2lem3  24692  shftmbl  24711  iundisj  24721  dyadmax  24771  dyadmbllem  24772  opnmbllem  24774  mdegmullem  25252  uc1pval  25313  mon1pval  25315  elqaalem1  25488  elqaalem3  25490  aannenlem2  25498  aalioulem2  25502  radcnvcl  25585  radcnvlt1  25586  radcnvle  25588  ftalem4  26234  ftalem5  26235  efnnfsumcl  26261  isppw  26272  sgmval2  26301  efchtdvds  26317  sqff1o  26340  fsumdvdsdiaglem  26341  fsumdvdsdiag  26342  fsumdvdscom  26343  musum  26349  muinv  26351  sgmmul  26358  ppiub  26361  vmasum  26373  logfac2  26374  perfectlem2  26387  lgsfcl  26462  lgscl  26468  lgsquadlem1  26537  lgsquadlem2  26538  rpvmasumlem  26644  mudivsum  26687  mulogsum  26689  mulog2sumlem2  26692  vmalogdivsum2  26695  logsqvma  26699  logsqvma2  26700  selberglem3  26704  selberg  26705  selberg34r  26728  pntsval2  26733  pntrlog2bndlem1  26734  tglnunirn  26918  tglnssp  26922  incistruhgr  27458  upgrss  27467  upgrn0  27468  upgruhgr  27481  usgrss  27553  uspgrushgr  27554  ushgredgedg  27605  ushgredgedgloop  27607  vtxdun  27857  vtxdginducedm1  27919  wlknwwlksnbij  28262  hashwwlksnext  28288  frcond3  28642  numclwlk1lem2  28743  ocsh  29654  spancl  29707  shsval2i  29758  ococin  29779  chsupid  29783  speccl  30270  hatomistici  30733  chpssati  30734  iundisjf  30937  aciunf1  31009  fpwrelmap  31077  iundisjfi  31126  pwrssmgc  31287  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem1  31402  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  nsgmgclem  31605  locfinreflem  31799  zarclsiin  31830  zarcls  31833  zartopn  31834  esumrnmpt2  32045  esumpinfval  32050  sigagensiga  32118  ldgenpisyslem1  32140  ldgenpisys  32143  measvuni  32191  imambfm  32238  dya2iocuni  32259  omscl  32271  oms0  32273  omsmon  32274  omssubadd  32276  carsgcl  32280  oddpwdc  32330  eulerpartlem1  32343  eulerpartlemt  32347  eulerpartgbij  32348  eulerpartlemmf  32351  eulerpartlemgh  32354  eulerpartlemgs2  32356  ballotlem2  32464  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemfmpn  32470  ballotlemiex  32477  ballotlemsup  32480  ballotlem7  32511  ballotth  32513  reprpmtf1o  32615  breprexplema  32619  hgt750lema  32646  bnj110  32847  bnj1204  33001  bnj1311  33013  fnrelpredd  33070  subfacp1lem6  33156  erdszelem2  33163  connpconn  33206  cvmliftmolem2  33253  cvmliftlem15  33269  cvmlift2lem12  33285  snmlff  33300  satfrnmapom  33341  tfisg  33795  sltval2  33868  conway  34002  eqscut2  34009  scutun12  34013  scutbdaybnd  34018  scutbdaybnd2  34019  scutbdaylt  34021  bday1s  34034  madef  34049  leftssold  34070  rightssold  34071  madebdaylemlrcut  34088  cofcut1  34099  cofcutr  34101  rankeq1o  34482  finminlem  34516  fnessref  34555  neibastop1  34557  neibastop2lem  34558  bj-rabtr  35127  bj-rabtrAUTO  35129  bj-vecssmod  35461  icoreresf  35532  phpreu  35770  fin2so  35773  poimirlem26  35812  poimirlem31  35817  poimirlem32  35818  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  ismblfin  35827  mbfposadd  35833  cnambfre  35834  cover2  35881  indexa  35900  fdc  35912  sstotbnd2  35941  sstotbnd3  35943  igenidl  36230  prnc  36234  toycom  36994  lkrlss  37116  atlatmstc  37340  atlatle  37341  glbconN  37398  linepsubN  37773  pmapssat  37780  pmaple  37782  pmapsub  37789  paddssat  37835  diass  39063  diaglbN  39076  diaintclN  39079  diassdvaN  39081  docaclN  39145  dibglbN  39187  dibintclN  39188  diclspsn  39215  dihglblem2N  39315  dih1dimatlem  39350  dihglb2  39363  dochval2  39373  dochcl  39374  dochvalr  39378  doch2val2  39385  dochss  39386  dochocss  39387  lclkr  39554  lclkrs  39560  lcdvbase  39614  lcdvbasess  39615  mapdunirnN  39671  aks4d1p4  40094  aks4d1p5  40095  aks4d1p7  40098  aks4d1p8  40102  sticksstones1  40109  mhpind  40290  prjcrv0  40477  infdesc  40487  mzpindd  40575  fiphp3d  40648  rencldnfilem  40649  irrapx1  40657  pellexlem3  40660  pellfundre  40710  pellfundge  40711  pellfundlb  40713  pellfundglb  40714  jm2.22  40824  jm2.23  40825  rpnnen3  40861  pwssplit4  40921  pwfi2f1o  40928  hbtlem6  40961  dgraalem  40977  dgraaub  40980  itgocn  40996  rgspncl  41001  rfovcnvf1od  41619  fsovfd  41627  fsovcnvlem  41628  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  uzwo4  42608  disjf1o  42736  icof  42766  allbutfiinf  42967  supminfxr  43011  supminfxr2  43016  fsumsupp0  43126  sumnnodd  43178  fnlimabslt  43227  liminfvalxr  43331  ioodvbdlimc1lem1  43479  dvnprodlem1  43494  dvnprodlem2  43495  stoweidlem14  43562  stoweidlem34  43582  stoweidlem44  43592  stoweidlem50  43598  stoweidlem51  43599  stoweidlem52  43600  stoweidlem57  43605  stoweidlem59  43607  fourierdlem19  43674  fourierdlem20  43675  fourierdlem25  43680  fourierdlem31  43686  fourierdlem37  43692  fourierdlem42  43697  fourierdlem51  43705  fourierdlem54  43708  fourierdlem64  43718  fourierdlem79  43733  elaa2lem  43781  etransclem16  43798  etransclem24  43806  etransclem31  43813  etransclem33  43815  etransclem34  43816  etransclem48  43830  salgencl  43878  salexct  43880  salgenuni  43883  subsaliuncllem  43903  meadjiunlem  44010  caragenss  44049  caratheodory  44073  ovnlecvr  44103  ovnsslelem  44105  ovnlerp  44107  ovn0lem  44110  ovnsubaddlem1  44115  hoidmv1lelem1  44136  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  ovnhoilem1  44146  ovnhoilem2  44147  ovnlecvr2  44155  ovncvr2  44156  opnvonmbllem2  44178  ovolval4lem1  44194  ovolval5lem3  44199  pimconstlt1  44247  pimiooltgt  44255  pimgtmnf2  44259  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  sssmf  44283  incsmflem  44286  smfaddlem1  44308  smfaddlem2  44309  decsmflem  44311  smflimlem1  44316  smflimlem2  44317  smflimlem3  44318  smfrec  44334  smfmullem4  44339  smfdiv  44342  smfsuplem1  44355  smfsuplem3  44357  smfinflem  44361  smflimsuplem1  44364  smflimsuplem7  44370  smfliminflem  44374  sprsymrelfolem1  44955  prmdvdsfmtnof1lem1  45047  prmdvdsfmtnof  45049  perfectALTVlem2  45185  rabsubmgmd  45356  mgmhmeql  45368  oddibas  45378  2zlidl  45503  2zrngbas  45505  2zrng0  45507  isclatd  46280  topclat  46295