Theorem ssrab3 4031

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

Syntax hints:   = wceq 1541  {crab 3396   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915

This theorem is referenced by:  dmmptss  6195  omsson  7808  oawordeulem  8477  ordtypelem2  9414  wemapso2lem  9447  wemapwe  9596  cplem1  9791  cofsmo  10169  fin23lem28  10240  fin23lem30  10242  isf32lem5  10257  isf32lem6  10258  isf32lem7  10259  isf32lem8  10260  hsmexlem4  10329  hsmexlem5  10330  hsmexlem6  10331  zorn2lem1  10396  zorn2lem3  10398  zorn2lem4  10399  zorn2lem5  10400  0nnq  10824  elpqn  10825  rpnnen1lem2  12879  rpssre  12902  01sqrexlem5  15157  dvdsflip  16232  divalglem2  16310  divalglem5  16312  divalglem8  16315  gcdcllem3  16416  bezoutlem2  16455  bezoutlem3  16456  maxprmfct  16624  phimullem  16694  eulerthlem2  16697  pclem  16754  infpn2  16829  prmreclem2  16833  prmreclem3  16834  prmreclem5  16836  4sqlem13  16873  4sqlem14  16874  4sqlem17  16877  4sqlem18  16878  vdwnnlem3  16913  ramcl2lem  16925  ramtcl  16926  ramtcl2  16927  ramtub  16928  imasdsval2  17424  gsumval1  18595  nmzsubg  19081  nmznsg  19084  conjnmz  19168  conjnmzb  19169  gastacl  19225  sylow1lem2  19515  sylow1lem3  19516  sylow1lem4  19517  sylow1lem5  19518  sylow2a  19535  sylow3lem2  19544  ablfacrplem  19983  ablfacrp2  19985  ablfac1eu  19991  pgpfaclem1  19999  ablfaclem2  20004  ablfaclem3  20005  nzrring  20435  lringnzr  20460  rrgeq0  20619  rrgss  20621  lspsolvlem  21083  lbsextlem2  21100  lbsextlem3  21101  lbsextlem4  21102  cygznlem2a  21508  psgnghm  21521  dsmmbase  21676  frlmsslsp  21737  psrbagconf1o  21870  psrass1lem  21873  mplbasss  21937  coe1mul2lem2  22185  mretopd  23010  hauscmplem  23324  ptcmplem1  23970  ptcmplem3  23972  tgpconncompeqg  24030  imasdsf1olem  24291  blcld  24423  icccmplem1  24741  icccmplem2  24742  icccmplem3  24743  rrxf  25331  ivthlem1  25382  ivthlem2  25383  ivthlem3  25384  ovolsslem  25415  ovolicc2lem3  25450  ovolicc2lem4  25451  ovolicc2lem5  25452  ovolicc2  25453  dyadmbllem  25530  dyadmbl  25531  iblmbf  25698  abelthlem4  26374  abelthlem6  26376  abelthlem9  26380  abelth  26381  dvatan  26875  atancn  26876  lgamucov  26978  lgamucov2  26979  ftalem3  27015  mpodvdsmulf1o  27134  fsumdvdsmul  27135  dvdsmulf1o  27136  fsumdvdsmulOLD  27137  lgsfcl2  27244  rpvmasum2  27453  dchrisum0re  27454  dchrisum0lema  27455  dchrisum0lem1b  27456  dchrisum0lem1  27457  dchrisum0lem2a  27458  dchrisum0lem2  27459  dchrisum0lem3  27460  dchrisum0  27461  pntlem3  27550  axcontlem2  28947  axcontlem7  28952  axcontlem8  28953  axcontlem10  28955  upgrreslem  29286  umgrreslem  29287  usgrres  29290  vtxdginducedm1lem2  29523  finsumvtxdg2ssteplem1  29528  clwwlksswrd  29971  frgrwopregbsn  30301  frgrwopreg1  30302  atssch  32327  partfun2  32663  fcobijfs  32710  fcobijfs2  32711  elrgspnlem1  33218  elrgspnlem2  33219  nsgmgc  33386  ssdifidllem  33430  ssdifidlprm  33432  ssmxidllem  33447  1arithufdlem2  33519  1arithufdlem4  33521  extvfvvcl  33588  mplmulmvr  33592  esplymhp  33610  esplyfv1  33611  esplysply  33613  esplyfval3  33614  esplyind  33615  eulerpartlemgvv  34412  reprpmtf1o  34662  hgt750lemb  34692  hgt750leme  34694  bnj1212  34834  bnj213  34917  bnj1286  35054  bnj1312  35093  bnj1523  35106  subfacp1lem3  35249  subfacp1lem5  35251  wlimss  35894  bj-smgrpssmgm  37335  bj-mndsssmgrp  37337  bj-cmnssmnd  37339  bj-grpssmnd  37341  aks6d1c6lem4  42289  readvcot  42485  evlsmhpvvval  42716  fglmod  43193  naddwordnexlem4  43521  scottss  44363  limcperiod  45755  cncfshift  45999  cncfperiod  46004  ovnsslelem  46685  ovolval5lem3  46779  uspgrlimlem2  48116  uspgrlim  48119