Theorem ssrab2 4056

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

Syntax hints:   ∧ wa 398   ∈ wcel 2114  {cab 2799  {crab 3142   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3943  df-ss 3952

This theorem is referenced by:  ssrab3  4057  ssrabeq  4059  iinrab2  4992  riinrab  5006  rabexg  5234  pwnss  5250  rabelpw  5253  frminex  5535  wereu2  5552  wfisg  6183  ssimaex  6748  f1oresrab  6889  weniso  7107  canth  7111  riotacl  7131  riotassuni  7154  onminesb  7513  onminsb  7514  onintrab  7516  onnminsb  7519  onminex  7522  tfis  7569  suppssdm  7843  fnsuppres  7857  oeeulem  8227  nnawordex  8263  pmvalg  8417  fineqvlem  8732  ordtypelem3  8984  ordtypelem4  8985  ordtypelem6  8987  hartogs  9008  card2on  9018  wdom2d  9044  oemapvali  9147  tz9.12lem1  9216  tz9.12lem3  9218  rankf  9223  cardf2  9372  cardid2  9382  cardmin2  9427  acni3  9473  dfac2a  9555  cofsmo  9691  coftr  9695  fin2i2  9740  isfin2-2  9741  enfin2i  9743  fin1a2lem11  9832  fin1a2lem12  9833  axdc3lem4  9875  ac6num  9901  ac6  9902  ondomon  9985  alephval2  9994  pwfseqlem1  10080  pwfseqlem3  10082  wunccl  10166  tskmcl  10263  fiminreOLD  11590  infm3  11600  uzf  12247  nnwos  12316  supminf  12336  zsupss  12338  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  ixxf  12749  fzf  12897  flval3  13186  rabssnn0fi  13355  expge0  13466  expge1  13467  hashbclem  13811  sqrlem3  14604  rlimrege0  14936  incexc2  15193  bitsf  15776  bitsfzolem  15783  sadadd2lem  15808  sadadd3  15810  sadcl  15811  smupf  15827  smuval2  15831  smupvallem  15832  smucl  15833  smueqlem  15839  lcmcllem  15940  lcmn0cl  15941  lcmledvds  15943  lcmfval  15965  lcmfcllem  15969  lcmfn0cl  15970  lcmfledvds  15976  phicl2  16105  phibnd  16108  hashdvds  16112  phiprmpw  16113  phimullem  16116  eulerth  16120  phisum  16127  odzcllem  16129  odzdvds  16132  prmreclem1  16252  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  hashbccl  16339  prmgaplem3  16389  prmgaplem4  16390  prdsds  16737  mrcflem  16877  isacs1i  16928  wunnat  17226  dmcoass  17326  lublecl  17599  lubid  17600  issubmd  17971  mhmeql  17990  cntzval  18451  cntzssv  18458  symgsssg  18595  symgfisg  18596  pmtrdifellem4  18607  odfval  18660  odlem1  18663  odlem2  18667  odngen  18702  gexlem1  18704  gexlem2  18707  sylow2alem2  18743  sylow2blem3  18747  oddvdssubg  18975  cyggex2  19017  ablfaclem3  19209  lssacs  19739  lspf  19746  asplss  20103  aspsubrg  20105  psrass1lem  20157  psrdi  20186  psrdir  20187  psrass23l  20188  psrass23  20190  resspsrmul  20197  mplbas  20209  mplsubglem  20214  mplsubrglem  20219  mplmonmul  20245  psropprmul  20406  ocvfval  20810  ocvval  20811  dsmmval2  20880  dsmmsubg  20887  scmatlss  21134  smadiadet  21279  pmatcoe1fsupp  21309  cpmatsubgpmat  21328  fctop  21612  cctop  21614  ppttop  21615  epttop  21617  clscld  21655  neips  21721  neiptopnei  21740  ordtbaslem  21796  ordtuni  21798  ordtcld1  21805  ordtcld2  21806  cnpfval  21842  iscnp2  21847  cmpcov2  21998  cmpsublem  22007  tgcmp  22009  conncompcld  22042  1stcfb  22053  2ndc1stc  22059  2ndcdisj  22064  finlocfin  22128  kgentopon  22146  xkotf  22193  txkgen  22260  xkococnlem  22267  imastopn  22328  kqffn  22333  opnfbas  22450  flimfnfcls  22636  alexsubALT  22659  ptcmplem2  22661  symgtgp  22714  tgpconncompeqg  22720  tgpconncomp  22721  ghmcnp  22723  tsmsfbas  22736  eltsms  22741  utoptop  22843  utopbas  22844  blfvalps  22993  blfps  23016  blf  23017  nmoffn  23320  nmofval  23323  nmogelb  23325  nmolb  23326  nmof  23328  ishtpy  23576  clsocv  23853  rrxnm  23994  rrxbasefi  24013  minveclem3b  24031  minveclem4  24035  ovolcl  24079  ovollb  24080  ovolgelb  24081  ovolge0  24082  ovolshftlem1  24110  ovolshft  24112  ovolscalem1  24114  ovolscalem2  24115  ovolsca  24116  ovolicc2lem3  24120  shftmbl  24139  iundisj  24149  dyadmax  24199  dyadmbllem  24200  opnmbllem  24202  mdegmullem  24672  uc1pval  24733  mon1pval  24735  elqaalem1  24908  elqaalem3  24910  aannenlem2  24918  aalioulem2  24922  radcnvcl  25005  radcnvlt1  25006  radcnvle  25008  ftalem4  25653  ftalem5  25654  efnnfsumcl  25680  isppw  25691  sgmval2  25720  efchtdvds  25736  sqff1o  25759  fsumdvdsdiaglem  25760  fsumdvdsdiag  25761  fsumdvdscom  25762  musum  25768  muinv  25770  sgmmul  25777  ppiub  25780  vmasum  25792  logfac2  25793  perfectlem2  25806  lgsfcl  25881  lgscl  25887  lgsquadlem1  25956  lgsquadlem2  25957  rpvmasumlem  26063  mudivsum  26106  mulogsum  26108  mulog2sumlem2  26111  vmalogdivsum2  26114  logsqvma  26118  logsqvma2  26119  selberglem3  26123  selberg  26124  selberg34r  26147  pntsval2  26152  pntrlog2bndlem1  26153  tglnunirn  26334  tglnssp  26338  incistruhgr  26864  upgrss  26873  upgrn0  26874  upgruhgr  26887  usgrss  26959  uspgrushgr  26960  ushgredgedg  27011  ushgredgedgloop  27013  vtxdun  27263  vtxdginducedm1  27325  wlknwwlksnbij  27666  hashwwlksnext  27693  frcond3  28048  numclwlk1lem2  28149  ocsh  29060  spancl  29113  shsval2i  29164  ococin  29185  chsupid  29189  speccl  29676  hatomistici  30139  chpssati  30140  iundisjf  30339  aciunf1  30408  fcobijfs  30459  fpwrelmap  30469  iundisjfi  30519  cycpmco2f1  30766  cycpmco2rn  30767  cycpmco2lem1  30768  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  locfinreflem  31104  esumrnmpt2  31327  esumpinfval  31332  sigagensiga  31400  ldgenpisyslem1  31422  ldgenpisys  31425  measvuni  31473  imambfm  31520  dya2iocuni  31541  omscl  31553  oms0  31555  omsmon  31556  omssubadd  31558  carsgcl  31562  oddpwdc  31612  eulerpartlem1  31625  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemmf  31633  eulerpartlemgh  31636  eulerpartlemgs2  31638  ballotlem2  31746  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemfmpn  31752  ballotlemiex  31759  ballotlemsup  31762  ballotlem7  31793  ballotth  31795  reprpmtf1o  31897  breprexplema  31901  hgt750lema  31928  bnj110  32130  bnj1204  32284  bnj1311  32296  subfacp1lem3  32429  subfacp1lem5  32431  subfacp1lem6  32432  erdszelem2  32439  connpconn  32482  cvmliftmolem2  32529  cvmliftlem15  32545  cvmlift2lem12  32561  snmlff  32576  satfrnmapom  32617  tfisg  33055  frpomin  33078  frpoinsg  33081  frinsg  33087  sltval2  33163  conway  33264  scutun12  33271  scutbdaybnd  33275  scutbdaylt  33276  rankeq1o  33632  finminlem  33666  fnessref  33705  neibastop1  33707  neibastop2lem  33708  bj-rabtr  34251  bj-rabtrAUTO  34253  bj-vecssmod  34566  icoreresf  34636  phpreu  34891  fin2so  34894  poimirlem26  34933  poimirlem31  34938  poimirlem32  34939  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  ismblfin  34948  mbfposadd  34954  cnambfre  34955  cover2  35004  indexa  35023  fdc  35035  sstotbnd2  35067  sstotbnd3  35069  igenidl  35356  prnc  35360  toycom  36124  lkrlss  36246  atlatmstc  36470  atlatle  36471  glbconN  36528  linepsubN  36903  pmapssat  36910  pmaple  36912  pmapsub  36919  paddssat  36965  diass  38193  diaglbN  38206  diaintclN  38209  diassdvaN  38211  docaclN  38275  dibglbN  38317  dibintclN  38318  diclspsn  38345  dihglblem2N  38445  dih1dimatlem  38480  dihglb2  38493  dochval2  38503  dochcl  38504  dochvalr  38508  doch2val2  38515  dochss  38516  dochocss  38517  lclkr  38684  lclkrs  38690  lcdvbase  38744  lcdvbasess  38745  mapdunirnN  38801  mzpindd  39392  fiphp3d  39465  rencldnfilem  39466  irrapx1  39474  pellexlem3  39477  pellfundre  39527  pellfundge  39528  pellfundlb  39530  pellfundglb  39531  jm2.22  39641  jm2.23  39642  rpnnen3  39678  pwssplit4  39738  pwfi2f1o  39745  hbtlem6  39778  dgraalem  39794  dgraaub  39797  itgocn  39813  rgspncl  39818  rfovcnvf1od  40399  fsovfd  40407  fsovcnvlem  40408  binomcxplemdvbinom  40734  binomcxplemcvg  40735  binomcxplemnotnn0  40737  uzwo4  41364  disjf1o  41501  icof  41531  allbutfiinf  41743  supminfxr  41789  supminfxr2  41794  fsumsupp0  41908  sumnnodd  41960  fnlimabslt  42009  liminfvalxr  42113  ioodvbdlimc1lem1  42265  dvnprodlem1  42280  dvnprodlem2  42281  stoweidlem14  42348  stoweidlem34  42368  stoweidlem44  42378  stoweidlem50  42384  stoweidlem51  42385  stoweidlem52  42386  stoweidlem57  42391  stoweidlem59  42393  fourierdlem19  42460  fourierdlem20  42461  fourierdlem25  42466  fourierdlem31  42472  fourierdlem37  42478  fourierdlem42  42483  fourierdlem51  42491  fourierdlem54  42494  fourierdlem64  42504  fourierdlem79  42519  elaa2lem  42567  etransclem16  42584  etransclem24  42592  etransclem31  42599  etransclem33  42601  etransclem34  42602  etransclem48  42616  salgencl  42664  salexct  42666  salgenuni  42669  subsaliuncllem  42689  meadjiunlem  42796  caragenss  42835  caratheodory  42859  ovnlecvr  42889  ovnsslelem  42891  ovnlerp  42893  ovn0lem  42896  ovnsubaddlem1  42901  hoidmv1lelem1  42922  hoidmv1lelem3  42924  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  ovnhoilem1  42932  ovnhoilem2  42933  ovnlecvr2  42941  ovncvr2  42942  opnvonmbllem2  42964  ovolval4lem1  42980  ovolval5lem3  42985  pimconstlt1  43032  pimltpnf  43033  pimiooltgt  43038  pimgtmnf2  43041  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  sssmf  43064  incsmflem  43067  smfaddlem1  43088  smfaddlem2  43089  decsmflem  43091  smflimlem1  43096  smflimlem2  43097  smflimlem3  43098  smfrec  43113  smfmullem4  43118  smfdiv  43121  smfsuplem1  43134  smfsuplem3  43136  smfinflem  43140  smflimsuplem1  43143  smflimsuplem7  43149  smfliminflem  43153  sprsymrelfolem1  43703  prmdvdsfmtnof1lem1  43795  prmdvdsfmtnof  43797  perfectALTVlem2  43936  rabsubmgmd  44107  mgmhmeql  44119  oddibas  44129  2zlidl  44254  2zrngbas  44256  2zrng0  44258