Theorem ssrab3 4039

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

This proof depends on syntax axioms:   = wceq 1570  {crab 3419   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925

This theorem is used by:  dmmptss  6247  omsson  7875  oawordeulem  8548  ordtypelem2  9491  wemapso2lem  9524  wemapwe  9676  scottss  9874  cplem1OLD  9890  cofsmo  10271  fin23lem28  10342  fin23lem30  10344  isf32lem5  10359  isf32lem6  10360  isf32lem7  10361  isf32lem8  10362  hsmexlem4  10431  hsmexlem5  10432  hsmexlem6  10433  zorn2lem1  10498  zorn2lem3  10500  zorn2lem4  10501  zorn2lem5  10502  0nnq  10927  elpqn  10928  rpnnen1lem2  13019  rpssre  13042  01sqrexlem5  15323  dvdsflip  16400  divalglem2  16478  divalglem5  16480  divalglem8  16483  gcdcllem3  16584  bezoutlem2  16623  bezoutlem3  16624  maxprmfct  16793  phimullem  16863  eulerthlem2  16866  pclem  16923  infpn2  16998  prmreclem2  17002  prmreclem3  17003  prmreclem5  17005  4sqlem13  17042  4sqlem14  17043  4sqlem17  17046  4sqlem18  17047  vdwnnlem3  17082  ramcl2lem  17094  ramtcl  17095  ramtcl2  17096  ramtub  17097  imasdsval2  17595  gsumval1  18770  nmzsubg  19262  nmznsg  19265  conjnmz  19353  conjnmzb  19354  gastacl  19410  sylow1lem2  19700  sylow1lem3  19701  sylow1lem4  19702  sylow1lem5  19703  sylow2a  19720  sylow3lem2  19729  ablfacrplem  20168  ablfacrp2  20170  ablfac1eu  20176  pgpfaclem1  20184  ablfaclem2  20189  ablfaclem3  20190  nzrring  20650  lringnzr  20677  rrgeq0  20836  rrgss  20838  lspsolvlem  21303  lbsextlem2  21320  lbsextlem3  21321  lbsextlem4  21322  ssdifidllem  21521  ssdifidlprm  21523  cygznlem2a  21754  psgnghm  21767  dsmmbase  21922  frlmsslsp  21983  psrbagconf1o  22116  psrass1lem  22120  mplbasss  22183  coe1mul2lem2  22466  mretopd  23286  hauscmplem  23600  ptcmplem1  24246  ptcmplem3  24248  tgpconncompeqg  24306  imasdsf1olem  24567  blcld  24699  icccmplem1  25017  icccmplem2  25018  icccmplem3  25019  rrxf  25597  ivthlem1  25647  ivthlem2  25648  ivthlem3  25649  ovolsslem  25680  ovolicc2lem3  25715  ovolicc2lem4  25716  ovolicc2lem5  25717  ovolicc2  25718  dyadmbllem  25795  dyadmbl  25796  iblmbf  25963  abelthlem4  26634  abelthlem6  26636  abelthlem9  26640  abelth  26641  dvatan  27137  atancn  27138  lgamucov  27239  lgamucov2  27240  ftalem3  27276  mpodvdsmulf1o  27395  fsumdvdsmul  27396  dvdsmulf1o  27397  lgsfcl2  27504  rpvmasum2  27713  dchrisum0re  27714  dchrisum0lema  27715  dchrisum0lem1b  27716  dchrisum0lem1  27717  dchrisum0lem2a  27718  dchrisum0lem2  27719  dchrisum0lem3  27720  dchrisum0  27721  pntlem3  27810  axcontlem2  29352  axcontlem7  29357  axcontlem8  29358  axcontlem10  29360  upgrreslem  29691  umgrreslem  29692  usgrres  29695  vtxdginducedm1lem2  29927  finsumvtxdg2ssteplem1  29932  clwwlksswrd  30375  frgrwopregbsn  30705  frgrwopreg1  30706  atssch  32732  partfun2  33058  fcobijfs  33103  fcobijfs2  33104  elrgspnlem1  33593  elrgspnlem2  33594  nsgmgc  33752  ssmxidllem  33787  1arithufdlem2  33866  1arithufdlem4  33868  extvfvvcl  33956  mplmulmvr  33960  psrmonprod  33973  esplymhp  33989  esplyfv1  33990  esplysply  33992  esplyfval3  33993  esplyind  33996  eulerpartlemgvv  34798  reprpmtf1o  35045  hgt750lemb  35075  hgt750leme  35077  bnj1212  35219  bnj213  35302  bnj1286  35439  bnj1312  35478  bnj1523  35491  subfacp1lem3  35695  subfacp1lem5  35697  wlimss  36340  bj-smgrpssmgm  37953  bj-mndsssmgrp  37955  bj-cmnssmnd  37957  bj-grpssmnd  37959  aks6d1c6lem4  42981  readvcot  43166  evlsmhpvvval  43368  fglmod  43841  naddwordnexlem4  44169  limcperiod  46385  cncfshift  46629  cncfperiod  46634  ovnsslelem  47315  ovolval5lem3  47409  uspgrlimlem2  48795  uspgrlim  48798