Theorem ssrab3 4037

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

Syntax hints:   = wceq 1570  {crab 3416   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923

This theorem is referenced by:  dmmptss  6244  omsson  7867  oawordeulem  8540  ordtypelem2  9482  wemapso2lem  9515  wemapwe  9667  scottss  9870  cplem1  9876  cofsmo  10254  fin23lem28  10325  fin23lem30  10327  isf32lem5  10342  isf32lem6  10343  isf32lem7  10344  isf32lem8  10345  hsmexlem4  10414  hsmexlem5  10415  hsmexlem6  10416  zorn2lem1  10481  zorn2lem3  10483  zorn2lem4  10484  zorn2lem5  10485  0nnq  10910  elpqn  10911  rpnnen1lem2  13002  rpssre  13025  01sqrexlem5  15299  dvdsflip  16376  divalglem2  16454  divalglem5  16456  divalglem8  16459  gcdcllem3  16560  bezoutlem2  16599  bezoutlem3  16600  maxprmfct  16769  phimullem  16839  eulerthlem2  16842  pclem  16899  infpn2  16974  prmreclem2  16978  prmreclem3  16979  prmreclem5  16981  4sqlem13  17018  4sqlem14  17019  4sqlem17  17022  4sqlem18  17023  vdwnnlem3  17058  ramcl2lem  17070  ramtcl  17071  ramtcl2  17072  ramtub  17073  imasdsval2  17571  gsumval1  18742  nmzsubg  19232  nmznsg  19235  conjnmz  19323  conjnmzb  19324  gastacl  19380  sylow1lem2  19670  sylow1lem3  19671  sylow1lem4  19672  sylow1lem5  19673  sylow2a  19690  sylow3lem2  19699  ablfacrplem  20138  ablfacrp2  20140  ablfac1eu  20146  pgpfaclem1  20154  ablfaclem2  20159  ablfaclem3  20160  nzrring  20600  lringnzr  20627  rrgeq0  20786  rrgss  20788  lspsolvlem  21247  lbsextlem2  21264  lbsextlem3  21265  lbsextlem4  21266  ssdifidllem  21465  ssdifidlprm  21467  cygznlem2a  21698  psgnghm  21711  dsmmbase  21866  frlmsslsp  21927  psrbagconf1o  22060  psrass1lem  22064  mplbasss  22127  coe1mul2lem2  22410  mretopd  23230  hauscmplem  23544  ptcmplem1  24190  ptcmplem3  24192  tgpconncompeqg  24250  imasdsf1olem  24511  blcld  24643  icccmplem1  24961  icccmplem2  24962  icccmplem3  24963  rrxf  25541  ivthlem1  25591  ivthlem2  25592  ivthlem3  25593  ovolsslem  25624  ovolicc2lem3  25659  ovolicc2lem4  25660  ovolicc2lem5  25661  ovolicc2  25662  dyadmbllem  25739  dyadmbl  25740  iblmbf  25907  abelthlem4  26578  abelthlem6  26580  abelthlem9  26584  abelth  26585  dvatan  27081  atancn  27082  lgamucov  27183  lgamucov2  27184  ftalem3  27220  mpodvdsmulf1o  27339  fsumdvdsmul  27340  dvdsmulf1o  27341  lgsfcl2  27448  rpvmasum2  27657  dchrisum0re  27658  dchrisum0lema  27659  dchrisum0lem1b  27660  dchrisum0lem1  27661  dchrisum0lem2a  27662  dchrisum0lem2  27663  dchrisum0lem3  27664  dchrisum0  27665  pntlem3  27754  axcontlem2  29296  axcontlem7  29301  axcontlem8  29302  axcontlem10  29304  upgrreslem  29635  umgrreslem  29636  usgrres  29639  vtxdginducedm1lem2  29871  finsumvtxdg2ssteplem1  29876  clwwlksswrd  30319  frgrwopregbsn  30649  frgrwopreg1  30650  atssch  32676  partfun2  33002  fcobijfs  33047  fcobijfs2  33048  elrgspnlem1  33543  elrgspnlem2  33544  nsgmgc  33702  ssmxidllem  33737  1arithufdlem2  33816  1arithufdlem4  33818  extvfvvcl  33906  mplmulmvr  33910  psrmonprod  33923  esplymhp  33939  esplyfv1  33940  esplysply  33942  esplyfval3  33943  esplyind  33946  eulerpartlemgvv  34747  reprpmtf1o  34994  hgt750lemb  35024  hgt750leme  35026  bnj1212  35168  bnj213  35251  bnj1286  35388  bnj1312  35427  bnj1523  35440  subfacp1lem3  35655  subfacp1lem5  35657  wlimss  36300  bj-smgrpssmgm  37893  bj-mndsssmgrp  37895  bj-cmnssmnd  37897  bj-grpssmnd  37899  aks6d1c6lem4  42921  readvcot  43106  evlsmhpvvval  43310  fglmod  43783  naddwordnexlem4  44111  limcperiod  46327  cncfshift  46571  cncfperiod  46576  ovnsslelem  47257  ovolval5lem3  47351  uspgrlimlem2  48737  uspgrlim  48740