Theorem ssrab3 4091

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

Syntax hints:   = wceq 1536  {crab 3432   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-ss 3979

This theorem is referenced by:  dmmptss  6262  omsson  7890  oawordeulem  8590  ordtypelem2  9556  wemapso2lem  9589  wemapwe  9734  cplem1  9926  cofsmo  10306  fin23lem28  10377  fin23lem30  10379  isf32lem5  10394  isf32lem6  10395  isf32lem7  10396  isf32lem8  10397  hsmexlem4  10466  hsmexlem5  10467  hsmexlem6  10468  zorn2lem1  10533  zorn2lem3  10535  zorn2lem4  10536  zorn2lem5  10537  0nnq  10961  elpqn  10962  rpnnen1lem2  13016  rpssre  13039  01sqrexlem5  15281  dvdsflip  16350  divalglem2  16428  divalglem5  16430  divalglem8  16433  gcdcllem3  16534  bezoutlem2  16573  bezoutlem3  16574  maxprmfct  16742  phimullem  16812  eulerthlem2  16815  pclem  16871  infpn2  16946  prmreclem2  16950  prmreclem3  16951  prmreclem5  16953  4sqlem13  16990  4sqlem14  16991  4sqlem17  16994  4sqlem18  16995  vdwnnlem3  17030  ramcl2lem  17042  ramtcl  17043  ramtcl2  17044  ramtub  17045  imasdsval2  17562  gsumval1  18708  nmzsubg  19195  nmznsg  19198  conjnmz  19282  conjnmzb  19283  gastacl  19339  sylow1lem2  19631  sylow1lem3  19632  sylow1lem4  19633  sylow1lem5  19634  sylow2a  19651  sylow3lem2  19660  ablfacrplem  20099  ablfacrp2  20101  ablfac1eu  20107  pgpfaclem1  20115  ablfaclem2  20120  ablfaclem3  20121  nzrring  20532  lringnzr  20557  rrgeq0  20716  rrgss  20718  lspsolvlem  21161  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  cygznlem2a  21603  psgnghm  21615  dsmmbase  21772  frlmsslsp  21833  psrbagconf1o  21966  psrass1lem  21969  mplbasss  22034  coe1mul2lem2  22286  mretopd  23115  hauscmplem  23429  ptcmplem1  24075  ptcmplem3  24077  tgpconncompeqg  24135  imasdsf1olem  24398  blcld  24533  icccmplem1  24857  icccmplem2  24858  icccmplem3  24859  rrxf  25448  ivthlem1  25499  ivthlem2  25500  ivthlem3  25501  ovolsslem  25532  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2lem5  25569  ovolicc2  25570  dyadmbllem  25647  dyadmbl  25648  iblmbf  25816  abelthlem4  26492  abelthlem6  26494  abelthlem9  26498  abelth  26499  dvatan  26992  atancn  26993  lgamucov  27095  lgamucov2  27096  ftalem3  27132  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  lgsfcl2  27361  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  dchrisum0  27578  pntlem3  27667  axcontlem2  28994  axcontlem7  28999  axcontlem8  29000  axcontlem10  29002  upgrreslem  29335  umgrreslem  29336  usgrres  29339  vtxdginducedm1lem2  29572  finsumvtxdg2ssteplem1  29577  clwwlksswrd  30015  frgrwopregbsn  30345  frgrwopreg1  30346  atssch  32371  fcobijfs  32740  elrgspnlem1  33231  elrgspnlem2  33232  nsgmgc  33419  ssdifidllem  33463  ssdifidlprm  33465  ssmxidllem  33480  1arithufdlem2  33552  1arithufdlem4  33554  eulerpartlemgvv  34357  reprpmtf1o  34619  hgt750lemb  34649  hgt750leme  34651  bnj1212  34791  bnj213  34874  bnj1286  35011  bnj1312  35050  bnj1523  35063  subfacp1lem3  35166  subfacp1lem5  35168  wlimss  35810  bj-smgrpssmgm  37250  bj-mndsssmgrp  37252  bj-cmnssmnd  37254  bj-grpssmnd  37256  aks6d1c6lem4  42154  evlsmhpvvval  42581  fglmod  43061  naddwordnexlem4  43390  scottss  44238  limcperiod  45583  cncfshift  45829  cncfperiod  45834  ovnsslelem  46515  ovolval5lem3  46609  uspgrlimlem2  47891  uspgrlim  47894