Theorem ssrab3 4056

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

Syntax hints:   = wceq 1533  {crab 3142   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3942  df-ss 3951

This theorem is referenced by:  dmmptss  6089  omsson  7578  oawordeulem  8174  ordtypelem2  8977  wemapso2lem  9010  wemapwe  9154  cplem1  9312  cofsmo  9685  fin23lem28  9756  fin23lem30  9758  isf32lem5  9773  isf32lem6  9774  isf32lem7  9775  isf32lem8  9776  hsmexlem4  9845  hsmexlem5  9846  hsmexlem6  9847  zorn2lem1  9912  zorn2lem3  9914  zorn2lem4  9915  zorn2lem5  9916  0nnq  10340  elpqn  10341  rpnnen1lem2  12370  rpssre  12390  sqrlem5  14600  dvdsflip  15661  divalglem2  15740  divalglem5  15742  divalglem8  15745  gcdcllem3  15844  bezoutlem2  15882  bezoutlem3  15883  maxprmfct  16047  phimullem  16110  eulerthlem2  16113  pclem  16169  infpn2  16243  prmreclem2  16247  prmreclem3  16248  prmreclem5  16250  4sqlem13  16287  4sqlem14  16288  4sqlem17  16291  4sqlem18  16292  vdwnnlem3  16327  ramcl2lem  16339  ramtcl  16340  ramtcl2  16341  ramtub  16342  imasdsval2  16783  gsumval1  17887  nmzsubg  18311  nmznsg  18314  conjnmz  18386  conjnmzb  18387  gastacl  18433  sylow1lem2  18718  sylow1lem3  18719  sylow1lem4  18720  sylow1lem5  18721  sylow2a  18738  sylow3lem2  18747  ablfacrplem  19181  ablfacrp2  19183  ablfac1eu  19189  pgpfaclem1  19197  ablfaclem2  19202  ablfaclem3  19203  lspsolvlem  19908  lbsextlem2  19925  lbsextlem3  19926  lbsextlem4  19927  rrgeq0  20057  rrgss  20059  psrbagconf1o  20148  psrass1lem  20151  mplbasss  20206  coe1mul2lem2  20430  cygznlem2a  20708  psgnghm  20718  dsmmbase  20873  frlmsslsp  20934  mretopd  21694  hauscmplem  22008  ptcmplem1  22654  ptcmplem3  22656  tgpconncompeqg  22714  imasdsf1olem  22977  blcld  23109  icccmplem1  23424  icccmplem2  23425  icccmplem3  23426  rrxf  23998  ivthlem1  24046  ivthlem2  24047  ivthlem3  24048  ovolsslem  24079  ovolicc2lem3  24114  ovolicc2lem4  24115  ovolicc2lem5  24116  ovolicc2  24117  dyadmbllem  24194  dyadmbl  24195  iblmbf  24362  abelthlem4  25016  abelthlem6  25018  abelthlem9  25022  abelth  25023  dvatan  25507  atancn  25508  lgamucov  25609  lgamucov2  25610  ftalem3  25646  dvdsmulf1o  25765  fsumdvdsmul  25766  lgsfcl2  25873  rpvmasum2  26082  dchrisum0re  26083  dchrisum0lema  26084  dchrisum0lem1b  26085  dchrisum0lem1  26086  dchrisum0lem2a  26087  dchrisum0lem2  26088  dchrisum0lem3  26089  dchrisum0  26090  pntlem3  26179  axcontlem2  26745  axcontlem7  26750  axcontlem8  26751  axcontlem10  26753  upgrreslem  27080  umgrreslem  27081  usgrres  27084  vtxdginducedm1lem2  27316  finsumvtxdg2ssteplem1  27321  clwwlksswrd  27759  frgrwopregbsn  28090  frgrwopreg1  28091  atssch  30114  ssmxidllem  30973  eulerpartlemgvv  31629  reprpmtf1o  31892  hgt750lemb  31922  hgt750leme  31924  bnj1212  32066  bnj213  32149  bnj1286  32286  bnj1312  32325  bnj1523  32338  wlimss  33111  bj-smgrpssmgm  34544  bj-mndsssmgrp  34546  bj-cmnssmnd  34548  bj-grpssmnd  34550  fglmod  39666  scottss  40572  limcperiod  41902  cncfshift  42150  cncfperiod  42155