MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrab3 Structured version   Visualization version   GIF version

Theorem ssrab3 4038
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
StepHypRef Expression
1 ssrab3.1 . 2 𝐵 = {𝑥𝐴𝜑}
2 ssrab2 4035 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
31, 2eqsstri 3976 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  {crab 3405  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-in 3915  df-ss 3925
This theorem is referenced by:  dmmptss  6191  omsson  7802  oawordeulem  8497  ordtypelem2  9451  wemapso2lem  9484  wemapwe  9629  cplem1  9821  cofsmo  10201  fin23lem28  10272  fin23lem30  10274  isf32lem5  10289  isf32lem6  10290  isf32lem7  10291  isf32lem8  10292  hsmexlem4  10361  hsmexlem5  10362  hsmexlem6  10363  zorn2lem1  10428  zorn2lem3  10430  zorn2lem4  10431  zorn2lem5  10432  0nnq  10856  elpqn  10857  rpnnen1lem2  12894  rpssre  12914  01sqrexlem5  15123  dvdsflip  16191  divalglem2  16269  divalglem5  16271  divalglem8  16274  gcdcllem3  16373  bezoutlem2  16413  bezoutlem3  16414  maxprmfct  16577  phimullem  16643  eulerthlem2  16646  pclem  16702  infpn2  16777  prmreclem2  16781  prmreclem3  16782  prmreclem5  16784  4sqlem13  16821  4sqlem14  16822  4sqlem17  16825  4sqlem18  16826  vdwnnlem3  16861  ramcl2lem  16873  ramtcl  16874  ramtcl2  16875  ramtub  16876  imasdsval2  17390  gsumval1  18530  nmzsubg  18958  nmznsg  18961  conjnmz  19033  conjnmzb  19034  gastacl  19080  sylow1lem2  19372  sylow1lem3  19373  sylow1lem4  19374  sylow1lem5  19375  sylow2a  19392  sylow3lem2  19401  ablfacrplem  19835  ablfacrp2  19837  ablfac1eu  19843  pgpfaclem1  19851  ablfaclem2  19856  ablfaclem3  19857  lspsolvlem  20588  lbsextlem2  20605  lbsextlem3  20606  lbsextlem4  20607  rrgeq0  20745  rrgss  20747  cygznlem2a  20959  psgnghm  20969  dsmmbase  21126  frlmsslsp  21187  psrbagconf1o  21323  psrbagconf1oOLD  21324  psrass1lemOLD  21327  psrass1lem  21330  mplbasss  21387  coe1mul2lem2  21623  mretopd  22427  hauscmplem  22741  ptcmplem1  23387  ptcmplem3  23389  tgpconncompeqg  23447  imasdsf1olem  23710  blcld  23845  icccmplem1  24169  icccmplem2  24170  icccmplem3  24171  rrxf  24749  ivthlem1  24799  ivthlem2  24800  ivthlem3  24801  ovolsslem  24832  ovolicc2lem3  24867  ovolicc2lem4  24868  ovolicc2lem5  24869  ovolicc2  24870  dyadmbllem  24947  dyadmbl  24948  iblmbf  25116  abelthlem4  25777  abelthlem6  25779  abelthlem9  25783  abelth  25784  dvatan  26269  atancn  26270  lgamucov  26371  lgamucov2  26372  ftalem3  26408  dvdsmulf1o  26527  fsumdvdsmul  26528  lgsfcl2  26635  rpvmasum2  26844  dchrisum0re  26845  dchrisum0lema  26846  dchrisum0lem1b  26847  dchrisum0lem1  26848  dchrisum0lem2a  26849  dchrisum0lem2  26850  dchrisum0lem3  26851  dchrisum0  26852  pntlem3  26941  axcontlem2  27800  axcontlem7  27805  axcontlem8  27806  axcontlem10  27808  upgrreslem  28138  umgrreslem  28139  usgrres  28142  vtxdginducedm1lem2  28374  finsumvtxdg2ssteplem1  28379  clwwlksswrd  28817  frgrwopregbsn  29147  frgrwopreg1  29148  atssch  31171  fcobijfs  31523  nsgmgc  32073  ssmxidllem  32117  eulerpartlemgvv  32845  reprpmtf1o  33108  hgt750lemb  33138  hgt750leme  33140  bnj1212  33280  bnj213  33363  bnj1286  33500  bnj1312  33539  bnj1523  33552  subfacp1lem3  33645  subfacp1lem5  33647  wlimss  34274  bj-smgrpssmgm  35706  bj-mndsssmgrp  35708  bj-cmnssmnd  35710  bj-grpssmnd  35712  fglmod  41338  scottss  42465  limcperiod  43801  cncfshift  44047  cncfperiod  44052  ovnsslelem  44733  ovolval5lem3  44827
  Copyright terms: Public domain W3C validator