Theorem ssrab3 4082

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

Syntax hints:   = wceq 1540  {crab 3436   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968

This theorem is referenced by:  dmmptss  6261  omsson  7891  oawordeulem  8592  ordtypelem2  9559  wemapso2lem  9592  wemapwe  9737  cplem1  9929  cofsmo  10309  fin23lem28  10380  fin23lem30  10382  isf32lem5  10397  isf32lem6  10398  isf32lem7  10399  isf32lem8  10400  hsmexlem4  10469  hsmexlem5  10470  hsmexlem6  10471  zorn2lem1  10536  zorn2lem3  10538  zorn2lem4  10539  zorn2lem5  10540  0nnq  10964  elpqn  10965  rpnnen1lem2  13019  rpssre  13042  01sqrexlem5  15285  dvdsflip  16354  divalglem2  16432  divalglem5  16434  divalglem8  16437  gcdcllem3  16538  bezoutlem2  16577  bezoutlem3  16578  maxprmfct  16746  phimullem  16816  eulerthlem2  16819  pclem  16876  infpn2  16951  prmreclem2  16955  prmreclem3  16956  prmreclem5  16958  4sqlem13  16995  4sqlem14  16996  4sqlem17  16999  4sqlem18  17000  vdwnnlem3  17035  ramcl2lem  17047  ramtcl  17048  ramtcl2  17049  ramtub  17050  imasdsval2  17561  gsumval1  18696  nmzsubg  19183  nmznsg  19186  conjnmz  19270  conjnmzb  19271  gastacl  19327  sylow1lem2  19617  sylow1lem3  19618  sylow1lem4  19619  sylow1lem5  19620  sylow2a  19637  sylow3lem2  19646  ablfacrplem  20085  ablfacrp2  20087  ablfac1eu  20093  pgpfaclem1  20101  ablfaclem2  20106  ablfaclem3  20107  nzrring  20516  lringnzr  20541  rrgeq0  20700  rrgss  20702  lspsolvlem  21144  lbsextlem2  21161  lbsextlem3  21162  lbsextlem4  21163  cygznlem2a  21586  psgnghm  21598  dsmmbase  21755  frlmsslsp  21816  psrbagconf1o  21949  psrass1lem  21952  mplbasss  22017  coe1mul2lem2  22271  mretopd  23100  hauscmplem  23414  ptcmplem1  24060  ptcmplem3  24062  tgpconncompeqg  24120  imasdsf1olem  24383  blcld  24518  icccmplem1  24844  icccmplem2  24845  icccmplem3  24846  rrxf  25435  ivthlem1  25486  ivthlem2  25487  ivthlem3  25488  ovolsslem  25519  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2lem5  25556  ovolicc2  25557  dyadmbllem  25634  dyadmbl  25635  iblmbf  25802  abelthlem4  26478  abelthlem6  26480  abelthlem9  26484  abelth  26485  dvatan  26978  atancn  26979  lgamucov  27081  lgamucov2  27082  ftalem3  27118  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  lgsfcl2  27347  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  dchrisum0  27564  pntlem3  27653  axcontlem2  28980  axcontlem7  28985  axcontlem8  28986  axcontlem10  28988  upgrreslem  29321  umgrreslem  29322  usgrres  29325  vtxdginducedm1lem2  29558  finsumvtxdg2ssteplem1  29563  clwwlksswrd  30006  frgrwopregbsn  30336  frgrwopreg1  30337  atssch  32362  fcobijfs  32734  elrgspnlem1  33246  elrgspnlem2  33247  nsgmgc  33440  ssdifidllem  33484  ssdifidlprm  33486  ssmxidllem  33501  1arithufdlem2  33573  1arithufdlem4  33575  eulerpartlemgvv  34378  reprpmtf1o  34641  hgt750lemb  34671  hgt750leme  34673  bnj1212  34813  bnj213  34896  bnj1286  35033  bnj1312  35072  bnj1523  35085  subfacp1lem3  35187  subfacp1lem5  35189  wlimss  35830  bj-smgrpssmgm  37269  bj-mndsssmgrp  37271  bj-cmnssmnd  37273  bj-grpssmnd  37275  aks6d1c6lem4  42174  readvcot  42394  evlsmhpvvval  42605  fglmod  43085  naddwordnexlem4  43414  scottss  44262  limcperiod  45643  cncfshift  45889  cncfperiod  45894  ovnsslelem  46575  ovolval5lem3  46669  uspgrlimlem2  47956  uspgrlim  47959