Theorem ssrab3 4033

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 4031	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
3	1, 2	eqsstri 3980	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1559  {crab 3413   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3919

This theorem is referenced by:  dmmptss  6222  omsson  7844  oawordeulem  8516  ordtypelem2  9460  wemapso2lem  9493  wemapwe  9645  cplem1  9840  cofsmo  10219  fin23lem28  10290  fin23lem30  10292  isf32lem5  10307  isf32lem6  10308  isf32lem7  10309  isf32lem8  10310  hsmexlem4  10379  hsmexlem5  10380  hsmexlem6  10381  zorn2lem1  10446  zorn2lem3  10448  zorn2lem4  10449  zorn2lem5  10450  0nnq  10875  elpqn  10876  rpnnen1lem2  12971  rpssre  12994  01sqrexlem5  15263  dvdsflip  16341  divalglem2  16419  divalglem5  16421  divalglem8  16424  gcdcllem3  16525  bezoutlem2  16564  bezoutlem3  16565  maxprmfct  16734  phimullem  16804  eulerthlem2  16807  pclem  16864  infpn2  16939  prmreclem2  16943  prmreclem3  16944  prmreclem5  16946  4sqlem13  16983  4sqlem14  16984  4sqlem17  16987  4sqlem18  16988  vdwnnlem3  17023  ramcl2lem  17035  ramtcl  17036  ramtcl2  17037  ramtub  17038  imasdsval2  17536  gsumval1  18707  nmzsubg  19196  nmznsg  19199  conjnmz  19282  conjnmzb  19283  gastacl  19339  sylow1lem2  19629  sylow1lem3  19630  sylow1lem4  19631  sylow1lem5  19632  sylow2a  19649  sylow3lem2  19658  ablfacrplem  20097  ablfacrp2  20099  ablfac1eu  20105  pgpfaclem1  20113  ablfaclem2  20118  ablfaclem3  20119  nzrring  20552  lringnzr  20577  rrgeq0  20736  rrgss  20738  lspsolvlem  21199  lbsextlem2  21216  lbsextlem3  21217  lbsextlem4  21218  cygznlem2a  21606  psgnghm  21619  dsmmbase  21774  frlmsslsp  21835  psrbagconf1o  21968  psrass1lem  21972  mplbasss  22035  coe1mul2lem2  22318  mretopd  23139  hauscmplem  23453  ptcmplem1  24099  ptcmplem3  24101  tgpconncompeqg  24159  imasdsf1olem  24420  blcld  24552  icccmplem1  24870  icccmplem2  24871  icccmplem3  24872  rrxf  25450  ivthlem1  25500  ivthlem2  25501  ivthlem3  25502  ovolsslem  25533  ovolicc2lem3  25568  ovolicc2lem4  25569  ovolicc2lem5  25570  ovolicc2  25571  dyadmbllem  25648  dyadmbl  25649  iblmbf  25816  abelthlem4  26484  abelthlem6  26486  abelthlem9  26490  abelth  26491  dvatan  26987  atancn  26988  lgamucov  27089  lgamucov2  27090  ftalem3  27126  mpodvdsmulf1o  27245  fsumdvdsmul  27246  dvdsmulf1o  27247  lgsfcl2  27354  rpvmasum2  27563  dchrisum0re  27564  dchrisum0lema  27565  dchrisum0lem1b  27566  dchrisum0lem1  27567  dchrisum0lem2a  27568  dchrisum0lem2  27569  dchrisum0lem3  27570  dchrisum0  27571  pntlem3  27660  axcontlem2  29122  axcontlem7  29127  axcontlem8  29128  axcontlem10  29130  upgrreslem  29461  umgrreslem  29462  usgrres  29465  vtxdginducedm1lem2  29697  finsumvtxdg2ssteplem1  29702  clwwlksswrd  30145  frgrwopregbsn  30475  frgrwopreg1  30476  atssch  32502  partfun2  32838  fcobijfs  32883  fcobijfs2  32884  elrgspnlem1  33383  elrgspnlem2  33384  nsgmgc  33558  ssdifidllem  33603  ssdifidlprm  33605  ssmxidllem  33621  1arithufdlem2  33701  1arithufdlem4  33703  extvfvvcl  33792  mplmulmvr  33796  psrmonprod  33809  esplymhp  33825  esplyfv1  33826  esplysply  33828  esplyfval3  33829  esplyind  33832  eulerpartlemgvv  34633  reprpmtf1o  34880  hgt750lemb  34910  hgt750leme  34912  bnj1212  35054  bnj213  35137  bnj1286  35274  bnj1312  35313  bnj1523  35326  subfacp1lem3  35492  subfacp1lem5  35494  wlimss  36137  bj-smgrpssmgm  37720  bj-mndsssmgrp  37722  bj-cmnssmnd  37724  bj-grpssmnd  37726  aks6d1c6lem4  42750  readvcot  42933  evlsmhpvvval  43137  fglmod  43610  naddwordnexlem4  43938  scottss  44779  limcperiod  46164  cncfshift  46408  cncfperiod  46413  ovnsslelem  47094  ovolval5lem3  47188  uspgrlimlem2  48571  uspgrlim  48574