Theorem ssrab3 4020

Description: Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
ssrab3.1	⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}

Assertion

Ref	Expression
ssrab3	⊢ 𝐵 ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem ssrab3

Step	Hyp	Ref	Expression
1		ssrab3.1	. 2 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}
2		ssrab2 4018	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
3	1, 2	eqsstri 3968	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1547  {crab 3392   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907

This theorem is referenced by:  dmmptss  6199  omsson  7817  oawordeulem  8486  ordtypelem2  9431  wemapso2lem  9464  wemapwe  9616  cplem1  9811  cofsmo  10189  fin23lem28  10260  fin23lem30  10262  isf32lem5  10277  isf32lem6  10278  isf32lem7  10279  isf32lem8  10280  hsmexlem4  10349  hsmexlem5  10350  hsmexlem6  10351  zorn2lem1  10416  zorn2lem3  10418  zorn2lem4  10419  zorn2lem5  10420  0nnq  10845  elpqn  10846  rpnnen1lem2  12925  rpssre  12948  01sqrexlem5  15206  dvdsflip  16284  divalglem2  16362  divalglem5  16364  divalglem8  16367  gcdcllem3  16468  bezoutlem2  16507  bezoutlem3  16508  maxprmfct  16677  phimullem  16747  eulerthlem2  16750  pclem  16807  infpn2  16882  prmreclem2  16886  prmreclem3  16887  prmreclem5  16889  4sqlem13  16926  4sqlem14  16927  4sqlem17  16930  4sqlem18  16931  vdwnnlem3  16966  ramcl2lem  16978  ramtcl  16979  ramtcl2  16980  ramtub  16981  imasdsval2  17478  gsumval1  18649  nmzsubg  19138  nmznsg  19141  conjnmz  19225  conjnmzb  19226  gastacl  19282  sylow1lem2  19572  sylow1lem3  19573  sylow1lem4  19574  sylow1lem5  19575  sylow2a  19592  sylow3lem2  19601  ablfacrplem  20040  ablfacrp2  20042  ablfac1eu  20048  pgpfaclem1  20056  ablfaclem2  20061  ablfaclem3  20062  nzrring  20495  lringnzr  20520  rrgeq0  20679  rrgss  20681  lspsolvlem  21142  lbsextlem2  21159  lbsextlem3  21160  lbsextlem4  21161  cygznlem2a  21549  psgnghm  21562  dsmmbase  21717  frlmsslsp  21778  psrbagconf1o  21911  psrass1lem  21915  mplbasss  21978  coe1mul2lem2  22261  mretopd  23082  hauscmplem  23396  ptcmplem1  24042  ptcmplem3  24044  tgpconncompeqg  24102  imasdsf1olem  24363  blcld  24495  icccmplem1  24813  icccmplem2  24814  icccmplem3  24815  rrxf  25393  ivthlem1  25443  ivthlem2  25444  ivthlem3  25445  ovolsslem  25476  ovolicc2lem3  25511  ovolicc2lem4  25512  ovolicc2lem5  25513  ovolicc2  25514  dyadmbllem  25591  dyadmbl  25592  iblmbf  25759  abelthlem4  26424  abelthlem6  26426  abelthlem9  26430  abelth  26431  dvatan  26924  atancn  26925  lgamucov  27026  lgamucov2  27027  ftalem3  27063  mpodvdsmulf1o  27182  fsumdvdsmul  27183  dvdsmulf1o  27184  lgsfcl2  27291  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lema  27502  dchrisum0lem1b  27503  dchrisum0lem1  27504  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0lem3  27507  dchrisum0  27508  pntlem3  27597  axcontlem2  29059  axcontlem7  29064  axcontlem8  29065  axcontlem10  29067  upgrreslem  29398  umgrreslem  29399  usgrres  29402  vtxdginducedm1lem2  29634  finsumvtxdg2ssteplem1  29639  clwwlksswrd  30082  frgrwopregbsn  30412  frgrwopreg1  30413  atssch  32439  partfun2  32775  fcobijfs  32820  fcobijfs2  32821  elrgspnlem1  33330  elrgspnlem2  33331  nsgmgc  33502  ssdifidllem  33546  ssdifidlprm  33548  ssmxidllem  33563  1arithufdlem2  33635  1arithufdlem4  33637  extvfvvcl  33726  mplmulmvr  33730  psrmonprod  33743  esplymhp  33759  esplyfv1  33760  esplysply  33762  esplyfval3  33763  esplyind  33766  eulerpartlemgvv  34567  reprpmtf1o  34817  hgt750lemb  34847  hgt750leme  34849  bnj1212  34988  bnj213  35071  bnj1286  35208  bnj1312  35247  bnj1523  35260  subfacp1lem3  35417  subfacp1lem5  35419  wlimss  36062  bj-smgrpssmgm  37635  bj-mndsssmgrp  37637  bj-cmnssmnd  37639  bj-grpssmnd  37641  aks6d1c6lem4  42665  readvcot  42848  evlsmhpvvval  43052  fglmod  43525  naddwordnexlem4  43853  scottss  44694  limcperiod  46080  cncfshift  46324  cncfperiod  46329  ovnsslelem  47010  ovolval5lem3  47104  uspgrlimlem2  48487  uspgrlim  48490