Theorem ssrab3 4081

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

Syntax hints:   = wceq 1542  {crab 3433   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  dmmptss  6241  omsson  7859  oawordeulem  8554  ordtypelem2  9514  wemapso2lem  9547  wemapwe  9692  cplem1  9884  cofsmo  10264  fin23lem28  10335  fin23lem30  10337  isf32lem5  10352  isf32lem6  10353  isf32lem7  10354  isf32lem8  10355  hsmexlem4  10424  hsmexlem5  10425  hsmexlem6  10426  zorn2lem1  10491  zorn2lem3  10493  zorn2lem4  10494  zorn2lem5  10495  0nnq  10919  elpqn  10920  rpnnen1lem2  12961  rpssre  12981  01sqrexlem5  15193  dvdsflip  16260  divalglem2  16338  divalglem5  16340  divalglem8  16343  gcdcllem3  16442  bezoutlem2  16482  bezoutlem3  16483  maxprmfct  16646  phimullem  16712  eulerthlem2  16715  pclem  16771  infpn2  16846  prmreclem2  16850  prmreclem3  16851  prmreclem5  16853  4sqlem13  16890  4sqlem14  16891  4sqlem17  16894  4sqlem18  16895  vdwnnlem3  16930  ramcl2lem  16942  ramtcl  16943  ramtcl2  16944  ramtub  16945  imasdsval2  17462  gsumval1  18602  nmzsubg  19045  nmznsg  19048  conjnmz  19126  conjnmzb  19127  gastacl  19173  sylow1lem2  19467  sylow1lem3  19468  sylow1lem4  19469  sylow1lem5  19470  sylow2a  19487  sylow3lem2  19496  ablfacrplem  19935  ablfacrp2  19937  ablfac1eu  19943  pgpfaclem1  19951  ablfaclem2  19956  ablfaclem3  19957  nzrring  20295  lringnzr  20311  lspsolvlem  20755  lbsextlem2  20772  lbsextlem3  20773  lbsextlem4  20774  rrgeq0  20906  rrgss  20908  cygznlem2a  21123  psgnghm  21133  dsmmbase  21290  frlmsslsp  21351  psrbagconf1o  21489  psrbagconf1oOLD  21490  psrass1lemOLD  21493  psrass1lem  21496  mplbasss  21556  coe1mul2lem2  21790  mretopd  22596  hauscmplem  22910  ptcmplem1  23556  ptcmplem3  23558  tgpconncompeqg  23616  imasdsf1olem  23879  blcld  24014  icccmplem1  24338  icccmplem2  24339  icccmplem3  24340  rrxf  24918  ivthlem1  24968  ivthlem2  24969  ivthlem3  24970  ovolsslem  25001  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2lem5  25038  ovolicc2  25039  dyadmbllem  25116  dyadmbl  25117  iblmbf  25285  abelthlem4  25946  abelthlem6  25948  abelthlem9  25952  abelth  25953  dvatan  26440  atancn  26441  lgamucov  26542  lgamucov2  26543  ftalem3  26579  dvdsmulf1o  26698  fsumdvdsmul  26699  lgsfcl2  26806  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  dchrisum0  27023  pntlem3  27112  axcontlem2  28223  axcontlem7  28228  axcontlem8  28229  axcontlem10  28231  upgrreslem  28561  umgrreslem  28562  usgrres  28565  vtxdginducedm1lem2  28797  finsumvtxdg2ssteplem1  28802  clwwlksswrd  29240  frgrwopregbsn  29570  frgrwopreg1  29571  atssch  31596  fcobijfs  31948  nsgmgc  32523  ssmxidllem  32589  eulerpartlemgvv  33375  reprpmtf1o  33638  hgt750lemb  33668  hgt750leme  33670  bnj1212  33810  bnj213  33893  bnj1286  34030  bnj1312  34069  bnj1523  34082  subfacp1lem3  34173  subfacp1lem5  34175  wlimss  34801  bj-smgrpssmgm  36149  bj-mndsssmgrp  36151  bj-cmnssmnd  36153  bj-grpssmnd  36155  evlsmhpvvval  41167  fglmod  41815  naddwordnexlem4  42152  scottss  43002  limcperiod  44344  cncfshift  44590  cncfperiod  44595  ovnsslelem  45276  ovolval5lem3  45370