Theorem ssrab3 4011

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

Syntax hints:   = wceq 1539  {crab 3067   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  dmmptss  6133  omsson  7691  oawordeulem  8347  ordtypelem2  9208  wemapso2lem  9241  wemapwe  9385  cplem1  9578  cofsmo  9956  fin23lem28  10027  fin23lem30  10029  isf32lem5  10044  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  hsmexlem4  10116  hsmexlem5  10117  hsmexlem6  10118  zorn2lem1  10183  zorn2lem3  10185  zorn2lem4  10186  zorn2lem5  10187  0nnq  10611  elpqn  10612  rpnnen1lem2  12646  rpssre  12666  sqrlem5  14886  dvdsflip  15954  divalglem2  16032  divalglem5  16034  divalglem8  16037  gcdcllem3  16136  bezoutlem2  16176  bezoutlem3  16177  maxprmfct  16342  phimullem  16408  eulerthlem2  16411  pclem  16467  infpn2  16542  prmreclem2  16546  prmreclem3  16547  prmreclem5  16549  4sqlem13  16586  4sqlem14  16587  4sqlem17  16590  4sqlem18  16591  vdwnnlem3  16626  ramcl2lem  16638  ramtcl  16639  ramtcl2  16640  ramtub  16641  imasdsval2  17144  gsumval1  18282  nmzsubg  18708  nmznsg  18711  conjnmz  18783  conjnmzb  18784  gastacl  18830  sylow1lem2  19119  sylow1lem3  19120  sylow1lem4  19121  sylow1lem5  19122  sylow2a  19139  sylow3lem2  19148  ablfacrplem  19583  ablfacrp2  19585  ablfac1eu  19591  pgpfaclem1  19599  ablfaclem2  19604  ablfaclem3  19605  lspsolvlem  20319  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  rrgeq0  20474  rrgss  20476  cygznlem2a  20687  psgnghm  20697  dsmmbase  20852  frlmsslsp  20913  psrbagconf1o  21049  psrbagconf1oOLD  21050  psrass1lemOLD  21053  psrass1lem  21056  mplbasss  21113  coe1mul2lem2  21349  mretopd  22151  hauscmplem  22465  ptcmplem1  23111  ptcmplem3  23113  tgpconncompeqg  23171  imasdsf1olem  23434  blcld  23567  icccmplem1  23891  icccmplem2  23892  icccmplem3  23893  rrxf  24470  ivthlem1  24520  ivthlem2  24521  ivthlem3  24522  ovolsslem  24553  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2lem5  24590  ovolicc2  24591  dyadmbllem  24668  dyadmbl  24669  iblmbf  24837  abelthlem4  25498  abelthlem6  25500  abelthlem9  25504  abelth  25505  dvatan  25990  atancn  25991  lgamucov  26092  lgamucov2  26093  ftalem3  26129  dvdsmulf1o  26248  fsumdvdsmul  26249  lgsfcl2  26356  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  pntlem3  26662  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  axcontlem10  27244  upgrreslem  27574  umgrreslem  27575  usgrres  27578  vtxdginducedm1lem2  27810  finsumvtxdg2ssteplem1  27815  clwwlksswrd  28252  frgrwopregbsn  28582  frgrwopreg1  28583  atssch  30606  fcobijfs  30960  nsgmgc  31499  ssmxidllem  31543  eulerpartlemgvv  32243  reprpmtf1o  32506  hgt750lemb  32536  hgt750leme  32538  bnj1212  32679  bnj213  32762  bnj1286  32899  bnj1312  32938  bnj1523  32951  subfacp1lem3  33044  subfacp1lem5  33046  wlimss  33750  bj-smgrpssmgm  35366  bj-mndsssmgrp  35368  bj-cmnssmnd  35370  bj-grpssmnd  35372  fglmod  40814  scottss  41750  limcperiod  43059  cncfshift  43305  cncfperiod  43310