Theorem ssrab3 4045

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

Syntax hints:   = wceq 1540  {crab 3405   ⊆ wss 3914

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931

This theorem is referenced by:  dmmptss  6214  omsson  7846  oawordeulem  8518  ordtypelem2  9472  wemapso2lem  9505  wemapwe  9650  cplem1  9842  cofsmo  10222  fin23lem28  10293  fin23lem30  10295  isf32lem5  10310  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  hsmexlem4  10382  hsmexlem5  10383  hsmexlem6  10384  zorn2lem1  10449  zorn2lem3  10451  zorn2lem4  10452  zorn2lem5  10453  0nnq  10877  elpqn  10878  rpnnen1lem2  12936  rpssre  12959  01sqrexlem5  15212  dvdsflip  16287  divalglem2  16365  divalglem5  16367  divalglem8  16370  gcdcllem3  16471  bezoutlem2  16510  bezoutlem3  16511  maxprmfct  16679  phimullem  16749  eulerthlem2  16752  pclem  16809  infpn2  16884  prmreclem2  16888  prmreclem3  16889  prmreclem5  16891  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwnnlem3  16968  ramcl2lem  16980  ramtcl  16981  ramtcl2  16982  ramtub  16983  imasdsval2  17479  gsumval1  18610  nmzsubg  19097  nmznsg  19100  conjnmz  19184  conjnmzb  19185  gastacl  19241  sylow1lem2  19529  sylow1lem3  19530  sylow1lem4  19531  sylow1lem5  19532  sylow2a  19549  sylow3lem2  19558  ablfacrplem  19997  ablfacrp2  19999  ablfac1eu  20005  pgpfaclem1  20013  ablfaclem2  20018  ablfaclem3  20019  nzrring  20425  lringnzr  20450  rrgeq0  20609  rrgss  20611  lspsolvlem  21052  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  cygznlem2a  21477  psgnghm  21489  dsmmbase  21644  frlmsslsp  21705  psrbagconf1o  21838  psrass1lem  21841  mplbasss  21906  coe1mul2lem2  22154  mretopd  22979  hauscmplem  23293  ptcmplem1  23939  ptcmplem3  23941  tgpconncompeqg  23999  imasdsf1olem  24261  blcld  24393  icccmplem1  24711  icccmplem2  24712  icccmplem3  24713  rrxf  25301  ivthlem1  25352  ivthlem2  25353  ivthlem3  25354  ovolsslem  25385  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  ovolicc2  25423  dyadmbllem  25500  dyadmbl  25501  iblmbf  25668  abelthlem4  26344  abelthlem6  26346  abelthlem9  26350  abelth  26351  dvatan  26845  atancn  26846  lgamucov  26948  lgamucov2  26949  ftalem3  26985  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  lgsfcl2  27214  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrisum0  27431  pntlem3  27520  axcontlem2  28892  axcontlem7  28897  axcontlem8  28898  axcontlem10  28900  upgrreslem  29231  umgrreslem  29232  usgrres  29235  vtxdginducedm1lem2  29468  finsumvtxdg2ssteplem1  29473  clwwlksswrd  29916  frgrwopregbsn  30246  frgrwopreg1  30247  atssch  32272  fcobijfs  32646  elrgspnlem1  33193  elrgspnlem2  33194  nsgmgc  33383  ssdifidllem  33427  ssdifidlprm  33429  ssmxidllem  33444  1arithufdlem2  33516  1arithufdlem4  33518  eulerpartlemgvv  34367  reprpmtf1o  34617  hgt750lemb  34647  hgt750leme  34649  bnj1212  34789  bnj213  34872  bnj1286  35009  bnj1312  35048  bnj1523  35061  subfacp1lem3  35169  subfacp1lem5  35171  wlimss  35817  bj-smgrpssmgm  37256  bj-mndsssmgrp  37258  bj-cmnssmnd  37260  bj-grpssmnd  37262  aks6d1c6lem4  42161  readvcot  42352  evlsmhpvvval  42583  fglmod  43062  naddwordnexlem4  43390  scottss  44232  limcperiod  45626  cncfshift  45872  cncfperiod  45877  ovnsslelem  46558  ovolval5lem3  46652  uspgrlimlem2  47988  uspgrlim  47991