Theorem ssrab3 4105

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

Syntax hints:   = wceq 1537  {crab 3443   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993

This theorem is referenced by:  dmmptss  6272  omsson  7907  oawordeulem  8610  ordtypelem2  9588  wemapso2lem  9621  wemapwe  9766  cplem1  9958  cofsmo  10338  fin23lem28  10409  fin23lem30  10411  isf32lem5  10426  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  hsmexlem4  10498  hsmexlem5  10499  hsmexlem6  10500  zorn2lem1  10565  zorn2lem3  10567  zorn2lem4  10568  zorn2lem5  10569  0nnq  10993  elpqn  10994  rpnnen1lem2  13042  rpssre  13064  01sqrexlem5  15295  dvdsflip  16365  divalglem2  16443  divalglem5  16445  divalglem8  16448  gcdcllem3  16547  bezoutlem2  16587  bezoutlem3  16588  maxprmfct  16756  phimullem  16826  eulerthlem2  16829  pclem  16885  infpn2  16960  prmreclem2  16964  prmreclem3  16965  prmreclem5  16967  4sqlem13  17004  4sqlem14  17005  4sqlem17  17008  4sqlem18  17009  vdwnnlem3  17044  ramcl2lem  17056  ramtcl  17057  ramtcl2  17058  ramtub  17059  imasdsval2  17576  gsumval1  18721  nmzsubg  19205  nmznsg  19208  conjnmz  19292  conjnmzb  19293  gastacl  19349  sylow1lem2  19641  sylow1lem3  19642  sylow1lem4  19643  sylow1lem5  19644  sylow2a  19661  sylow3lem2  19670  ablfacrplem  20109  ablfacrp2  20111  ablfac1eu  20117  pgpfaclem1  20125  ablfaclem2  20130  ablfaclem3  20131  nzrring  20542  lringnzr  20567  rrgeq0  20722  rrgss  20724  lspsolvlem  21167  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  cygznlem2a  21609  psgnghm  21621  dsmmbase  21778  frlmsslsp  21839  psrbagconf1o  21972  psrass1lem  21975  mplbasss  22040  coe1mul2lem2  22292  mretopd  23121  hauscmplem  23435  ptcmplem1  24081  ptcmplem3  24083  tgpconncompeqg  24141  imasdsf1olem  24404  blcld  24539  icccmplem1  24863  icccmplem2  24864  icccmplem3  24865  rrxf  25454  ivthlem1  25505  ivthlem2  25506  ivthlem3  25507  ovolsslem  25538  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2lem5  25575  ovolicc2  25576  dyadmbllem  25653  dyadmbl  25654  iblmbf  25822  abelthlem4  26496  abelthlem6  26498  abelthlem9  26502  abelth  26503  dvatan  26996  atancn  26997  lgamucov  27099  lgamucov2  27100  ftalem3  27136  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  lgsfcl2  27365  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0lem3  27581  dchrisum0  27582  pntlem3  27671  axcontlem2  28998  axcontlem7  29003  axcontlem8  29004  axcontlem10  29006  upgrreslem  29339  umgrreslem  29340  usgrres  29343  vtxdginducedm1lem2  29576  finsumvtxdg2ssteplem1  29581  clwwlksswrd  30019  frgrwopregbsn  30349  frgrwopreg1  30350  atssch  32375  fcobijfs  32737  nsgmgc  33405  ssdifidllem  33449  ssdifidlprm  33451  ssmxidllem  33466  1arithufdlem2  33538  1arithufdlem4  33540  eulerpartlemgvv  34341  reprpmtf1o  34603  hgt750lemb  34633  hgt750leme  34635  bnj1212  34775  bnj213  34858  bnj1286  34995  bnj1312  35034  bnj1523  35047  subfacp1lem3  35150  subfacp1lem5  35152  wlimss  35793  bj-smgrpssmgm  37234  bj-mndsssmgrp  37236  bj-cmnssmnd  37238  bj-grpssmnd  37240  aks6d1c6lem4  42130  evlsmhpvvval  42550  fglmod  43030  naddwordnexlem4  43363  scottss  44212  limcperiod  45549  cncfshift  45795  cncfperiod  45800  ovnsslelem  46481  ovolval5lem3  46575  uspgrlimlem2  47813  uspgrlim  47816