Theorem ssrab3 4035

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

Syntax hints:   = wceq 1542  {crab 3400   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-ss 3919

This theorem is referenced by:  dmmptss  6200  omsson  7814  oawordeulem  8483  ordtypelem2  9428  wemapso2lem  9461  wemapwe  9610  cplem1  9805  cofsmo  10183  fin23lem28  10254  fin23lem30  10256  isf32lem5  10271  isf32lem6  10272  isf32lem7  10273  isf32lem8  10274  hsmexlem4  10343  hsmexlem5  10344  hsmexlem6  10345  zorn2lem1  10410  zorn2lem3  10412  zorn2lem4  10413  zorn2lem5  10414  0nnq  10839  elpqn  10840  rpnnen1lem2  12894  rpssre  12917  01sqrexlem5  15173  dvdsflip  16248  divalglem2  16326  divalglem5  16328  divalglem8  16331  gcdcllem3  16432  bezoutlem2  16471  bezoutlem3  16472  maxprmfct  16640  phimullem  16710  eulerthlem2  16713  pclem  16770  infpn2  16845  prmreclem2  16849  prmreclem3  16850  prmreclem5  16852  4sqlem13  16889  4sqlem14  16890  4sqlem17  16893  4sqlem18  16894  vdwnnlem3  16929  ramcl2lem  16941  ramtcl  16942  ramtcl2  16943  ramtub  16944  imasdsval2  17441  gsumval1  18612  nmzsubg  19098  nmznsg  19101  conjnmz  19185  conjnmzb  19186  gastacl  19242  sylow1lem2  19532  sylow1lem3  19533  sylow1lem4  19534  sylow1lem5  19535  sylow2a  19552  sylow3lem2  19561  ablfacrplem  20000  ablfacrp2  20002  ablfac1eu  20008  pgpfaclem1  20016  ablfaclem2  20021  ablfaclem3  20022  nzrring  20453  lringnzr  20478  rrgeq0  20637  rrgss  20639  lspsolvlem  21101  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  cygznlem2a  21526  psgnghm  21539  dsmmbase  21694  frlmsslsp  21755  psrbagconf1o  21889  psrass1lem  21892  mplbasss  21956  coe1mul2lem2  22214  mretopd  23040  hauscmplem  23354  ptcmplem1  24000  ptcmplem3  24002  tgpconncompeqg  24060  imasdsf1olem  24321  blcld  24453  icccmplem1  24771  icccmplem2  24772  icccmplem3  24773  rrxf  25361  ivthlem1  25412  ivthlem2  25413  ivthlem3  25414  ovolsslem  25445  ovolicc2lem3  25480  ovolicc2lem4  25481  ovolicc2lem5  25482  ovolicc2  25483  dyadmbllem  25560  dyadmbl  25561  iblmbf  25728  abelthlem4  26404  abelthlem6  26406  abelthlem9  26410  abelth  26411  dvatan  26905  atancn  26906  lgamucov  27008  lgamucov2  27009  ftalem3  27045  mpodvdsmulf1o  27164  fsumdvdsmul  27165  dvdsmulf1o  27166  fsumdvdsmulOLD  27167  lgsfcl2  27274  rpvmasum2  27483  dchrisum0re  27484  dchrisum0lema  27485  dchrisum0lem1b  27486  dchrisum0lem1  27487  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0lem3  27490  dchrisum0  27491  pntlem3  27580  axcontlem2  29021  axcontlem7  29026  axcontlem8  29027  axcontlem10  29029  upgrreslem  29360  umgrreslem  29361  usgrres  29364  vtxdginducedm1lem2  29597  finsumvtxdg2ssteplem1  29602  clwwlksswrd  30045  frgrwopregbsn  30375  frgrwopreg1  30376  atssch  32401  partfun2  32736  fcobijfs  32781  fcobijfs2  32782  elrgspnlem1  33305  elrgspnlem2  33306  nsgmgc  33474  ssdifidllem  33518  ssdifidlprm  33520  ssmxidllem  33535  1arithufdlem2  33607  1arithufdlem4  33609  extvfvvcl  33681  mplmulmvr  33685  esplymhp  33707  esplyfv1  33708  esplysply  33710  esplyfval3  33711  esplyind  33712  eulerpartlemgvv  34514  reprpmtf1o  34764  hgt750lemb  34794  hgt750leme  34796  bnj1212  34936  bnj213  35019  bnj1286  35156  bnj1312  35195  bnj1523  35208  subfacp1lem3  35357  subfacp1lem5  35359  wlimss  36002  bj-smgrpssmgm  37444  bj-mndsssmgrp  37446  bj-cmnssmnd  37448  bj-grpssmnd  37450  aks6d1c6lem4  42464  readvcot  42655  evlsmhpvvval  42874  fglmod  43351  naddwordnexlem4  43679  scottss  44520  limcperiod  45910  cncfshift  46154  cncfperiod  46159  ovnsslelem  46840  ovolval5lem3  46934  uspgrlimlem2  48271  uspgrlim  48274