Theorem ssrab3 4016

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

Syntax hints:   = wceq 1539  {crab 3069   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  dmmptss  6149  omsson  7725  oawordeulem  8394  ordtypelem2  9287  wemapso2lem  9320  wemapwe  9464  cplem1  9656  cofsmo  10034  fin23lem28  10105  fin23lem30  10107  isf32lem5  10122  isf32lem6  10123  isf32lem7  10124  isf32lem8  10125  hsmexlem4  10194  hsmexlem5  10195  hsmexlem6  10196  zorn2lem1  10261  zorn2lem3  10263  zorn2lem4  10264  zorn2lem5  10265  0nnq  10689  elpqn  10690  rpnnen1lem2  12726  rpssre  12746  sqrlem5  14967  dvdsflip  16035  divalglem2  16113  divalglem5  16115  divalglem8  16118  gcdcllem3  16217  bezoutlem2  16257  bezoutlem3  16258  maxprmfct  16423  phimullem  16489  eulerthlem2  16492  pclem  16548  infpn2  16623  prmreclem2  16627  prmreclem3  16628  prmreclem5  16630  4sqlem13  16667  4sqlem14  16668  4sqlem17  16671  4sqlem18  16672  vdwnnlem3  16707  ramcl2lem  16719  ramtcl  16720  ramtcl2  16721  ramtub  16722  imasdsval2  17236  gsumval1  18376  nmzsubg  18802  nmznsg  18805  conjnmz  18877  conjnmzb  18878  gastacl  18924  sylow1lem2  19213  sylow1lem3  19214  sylow1lem4  19215  sylow1lem5  19216  sylow2a  19233  sylow3lem2  19242  ablfacrplem  19677  ablfacrp2  19679  ablfac1eu  19685  pgpfaclem1  19693  ablfaclem2  19698  ablfaclem3  19699  lspsolvlem  20413  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  rrgeq0  20570  rrgss  20572  cygznlem2a  20784  psgnghm  20794  dsmmbase  20951  frlmsslsp  21012  psrbagconf1o  21148  psrbagconf1oOLD  21149  psrass1lemOLD  21152  psrass1lem  21155  mplbasss  21212  coe1mul2lem2  21448  mretopd  22252  hauscmplem  22566  ptcmplem1  23212  ptcmplem3  23214  tgpconncompeqg  23272  imasdsf1olem  23535  blcld  23670  icccmplem1  23994  icccmplem2  23995  icccmplem3  23996  rrxf  24574  ivthlem1  24624  ivthlem2  24625  ivthlem3  24626  ovolsslem  24657  ovolicc2lem3  24692  ovolicc2lem4  24693  ovolicc2lem5  24694  ovolicc2  24695  dyadmbllem  24772  dyadmbl  24773  iblmbf  24941  abelthlem4  25602  abelthlem6  25604  abelthlem9  25608  abelth  25609  dvatan  26094  atancn  26095  lgamucov  26196  lgamucov2  26197  ftalem3  26233  dvdsmulf1o  26352  fsumdvdsmul  26353  lgsfcl2  26460  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  dchrisum0  26677  pntlem3  26766  axcontlem2  27342  axcontlem7  27347  axcontlem8  27348  axcontlem10  27350  upgrreslem  27680  umgrreslem  27681  usgrres  27684  vtxdginducedm1lem2  27916  finsumvtxdg2ssteplem1  27921  clwwlksswrd  28360  frgrwopregbsn  28690  frgrwopreg1  28691  atssch  30714  fcobijfs  31067  nsgmgc  31606  ssmxidllem  31650  eulerpartlemgvv  32352  reprpmtf1o  32615  hgt750lemb  32645  hgt750leme  32647  bnj1212  32788  bnj213  32871  bnj1286  33008  bnj1312  33047  bnj1523  33060  subfacp1lem3  33153  subfacp1lem5  33155  wlimss  33832  bj-smgrpssmgm  35448  bj-mndsssmgrp  35450  bj-cmnssmnd  35452  bj-grpssmnd  35454  fglmod  40905  scottss  41868  limcperiod  43176  cncfshift  43422  cncfperiod  43427