Theorem ssrab3 4010

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

This proof depends on syntax axioms:   = wceq 1570  {crab 3416   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901

This theorem is used by:  dmmptss  6256  omsson  7908  oawordeulem  8593  ordtypelem2  9543  wemapso2lem  9576  wemapwe  9728  scottss  9965  cplem1OLD  9981  cofsmo  10377  fin23lem28  10448  fin23lem30  10450  isf32lem5  10465  isf32lem6  10466  isf32lem7  10467  isf32lem8  10468  hsmexlem4  10537  hsmexlem5  10538  hsmexlem6  10539  zorn2lem1  10604  zorn2lem3  10606  zorn2lem4  10607  zorn2lem5  10608  0nnq  11039  elpqn  11040  rpnnen1lem2  13135  rpssre  13158  01sqrexlem5  15445  dvdsflip  16519  divalglem2  16597  divalglem5  16599  divalglem8  16602  gcdcllem3  16703  bezoutlem2  16745  bezoutlem3  16746  maxprmfct  16917  phimullem  16988  eulerthlem2  16991  pclem  17048  infpn2  17123  prmreclem2  17127  prmreclem3  17128  prmreclem5  17130  4sqlem13  17167  4sqlem14  17168  4sqlem17  17171  4sqlem18  17172  vdwnnlem3  17207  ramcl2lem  17219  ramtcl  17220  ramtcl2  17221  ramtub  17222  imasdsval2  17720  gsumval1  18904  nmzsubg  19407  nmznsg  19410  conjnmz  19498  conjnmzb  19499  gastacl  19556  sylow1lem2  19846  sylow1lem3  19847  sylow1lem4  19848  sylow1lem5  19849  sylow2a  19866  sylow3lem2  19875  ablfacrplem  20314  ablfacrp2  20316  ablfac1eu  20322  pgpfaclem1  20330  ablfaclem2  20335  ablfaclem3  20336  nzrring  20799  lringnzr  20826  rrgeq0  20985  rrgss  20987  lspsolvlem  21453  lbsextlem2  21470  lbsextlem3  21471  lbsextlem4  21472  ssdifidllem  21673  ssdifidlprm  21675  cygznlem2a  21906  psgnghm  21919  dsmmbase  22074  frlmsslsp  22135  psrbagconf1o  22270  psrass1lem  22274  mplbasss  22337  coe1mul2lem2  22620  mretopd  23443  hauscmplem  23757  ptcmplem1  24404  ptcmplem3  24406  tgpconncompeqg  24464  imasdsf1olem  24725  blcld  24857  icccmplem1  25175  icccmplem2  25176  icccmplem3  25177  rrxf  25755  ivthlem1  25805  ivthlem2  25806  ivthlem3  25807  ovolsslem  25838  ovolicc2lem3  25873  ovolicc2lem4  25874  ovolicc2lem5  25875  ovolicc2  25876  dyadmbllem  25953  dyadmbl  25954  iblmbf  26121  abelthlem4  26794  abelthlem6  26796  abelthlem9  26800  abelth  26801  dvatan  27296  atancn  27297  lgamucov  27398  lgamucov2  27399  ftalem3  27435  mpodvdsmulf1o  27554  fsumdvdsmul  27555  dvdsmulf1o  27556  lgsfcl2  27663  rpvmasum2  27872  dchrisum0re  27873  dchrisum0lema  27874  dchrisum0lem1b  27875  dchrisum0lem1  27876  dchrisum0lem2a  27877  dchrisum0lem2  27878  dchrisum0lem3  27879  dchrisum0  27880  pntlem3  27969  elcgrabasi  29408  axcontlem2  29576  axcontlem7  29581  axcontlem8  29582  axcontlem10  29584  upgrreslem  29918  umgrreslem  29919  usgrres  29922  vtxdginducedm1lem2  30154  finsumvtxdg2ssteplem1  30159  clwwlksswrd  30611  frgrwopregbsn  30951  frgrwopreg1  30952  atssch  32978  partfun2  33344  fcobijfs  33386  fcobijfs2  33387  elrgspnlem1  33879  elrgspnlem2  33880  nsgmgc  34047  ssmxidllem  34082  1arithufdlem2  34161  1arithufdlem4  34163  extvfvvcl  34250  mplmulmvr  34254  psrmonprod  34267  esplymhp  34283  esplyfv1  34284  esplysply  34286  esplyfval3  34287  esplyind  34290  eulerpartlemgvv  35091  reprpmtf1o  35338  hgt750lemb  35368  hgt750leme  35370  bnj1212  35512  bnj213  35595  bnj1286  35732  bnj1312  35771  bnj1523  35784  subfacp1lem3  36127  subfacp1lem5  36129  wlimss  36782  bj-smgrpssmgm  38394  bj-mndsssmgrp  38396  bj-cmnssmnd  38398  bj-grpssmnd  38400  aks6d1c6lem4  43426  readvcot  43619  evlsmhpvvval  43827  fglmod  44279  naddwordnexlem4  44606  limcperiod  46855  cncfshift  47099  cncfperiod  47104  ovnsslelem  47785  ovolval5lem3  47879  uspgrlimlem2  49302  uspgrlim  49305