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

Theorem ssrab3 4012
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 4010 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
31, 2eqsstri 3952 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  {crab 3068  wss 3883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-in 3890  df-ss 3900
This theorem is referenced by:  dmmptss  6122  omsson  7670  oawordeulem  8306  ordtypelem2  9165  wemapso2lem  9198  wemapwe  9342  cplem1  9535  cofsmo  9913  fin23lem28  9984  fin23lem30  9986  isf32lem5  10001  isf32lem6  10002  isf32lem7  10003  isf32lem8  10004  hsmexlem4  10073  hsmexlem5  10074  hsmexlem6  10075  zorn2lem1  10140  zorn2lem3  10142  zorn2lem4  10143  zorn2lem5  10144  0nnq  10568  elpqn  10569  rpnnen1lem2  12603  rpssre  12623  sqrlem5  14843  dvdsflip  15911  divalglem2  15989  divalglem5  15991  divalglem8  15994  gcdcllem3  16093  bezoutlem2  16133  bezoutlem3  16134  maxprmfct  16299  phimullem  16365  eulerthlem2  16368  pclem  16424  infpn2  16499  prmreclem2  16503  prmreclem3  16504  prmreclem5  16506  4sqlem13  16543  4sqlem14  16544  4sqlem17  16547  4sqlem18  16548  vdwnnlem3  16583  ramcl2lem  16595  ramtcl  16596  ramtcl2  16597  ramtub  16598  imasdsval2  17054  gsumval1  18188  nmzsubg  18614  nmznsg  18617  conjnmz  18689  conjnmzb  18690  gastacl  18736  sylow1lem2  19021  sylow1lem3  19022  sylow1lem4  19023  sylow1lem5  19024  sylow2a  19041  sylow3lem2  19050  ablfacrplem  19485  ablfacrp2  19487  ablfac1eu  19493  pgpfaclem1  19501  ablfaclem2  19506  ablfaclem3  19507  lspsolvlem  20212  lbsextlem2  20229  lbsextlem3  20230  lbsextlem4  20231  rrgeq0  20361  rrgss  20363  cygznlem2a  20565  psgnghm  20575  dsmmbase  20730  frlmsslsp  20791  psrbagconf1o  20927  psrbagconf1oOLD  20928  psrass1lemOLD  20931  psrass1lem  20934  mplbasss  20991  coe1mul2lem2  21221  mretopd  22021  hauscmplem  22335  ptcmplem1  22981  ptcmplem3  22983  tgpconncompeqg  23041  imasdsf1olem  23303  blcld  23435  icccmplem1  23751  icccmplem2  23752  icccmplem3  23753  rrxf  24330  ivthlem1  24380  ivthlem2  24381  ivthlem3  24382  ovolsslem  24413  ovolicc2lem3  24448  ovolicc2lem4  24449  ovolicc2lem5  24450  ovolicc2  24451  dyadmbllem  24528  dyadmbl  24529  iblmbf  24697  abelthlem4  25358  abelthlem6  25360  abelthlem9  25364  abelth  25365  dvatan  25850  atancn  25851  lgamucov  25952  lgamucov2  25953  ftalem3  25989  dvdsmulf1o  26108  fsumdvdsmul  26109  lgsfcl2  26216  rpvmasum2  26425  dchrisum0re  26426  dchrisum0lema  26427  dchrisum0lem1b  26428  dchrisum0lem1  26429  dchrisum0lem2a  26430  dchrisum0lem2  26431  dchrisum0lem3  26432  dchrisum0  26433  pntlem3  26522  axcontlem2  27088  axcontlem7  27093  axcontlem8  27094  axcontlem10  27096  upgrreslem  27424  umgrreslem  27425  usgrres  27428  vtxdginducedm1lem2  27660  finsumvtxdg2ssteplem1  27665  clwwlksswrd  28102  frgrwopregbsn  28432  frgrwopreg1  28433  atssch  30456  fcobijfs  30810  nsgmgc  31343  ssmxidllem  31387  eulerpartlemgvv  32087  reprpmtf1o  32350  hgt750lemb  32380  hgt750leme  32382  bnj1212  32523  bnj213  32606  bnj1286  32743  bnj1312  32782  bnj1523  32795  subfacp1lem3  32888  subfacp1lem5  32890  wlimss  33594  bj-smgrpssmgm  35210  bj-mndsssmgrp  35212  bj-cmnssmnd  35214  bj-grpssmnd  35216  fglmod  40649  scottss  41582  limcperiod  42890  cncfshift  43136  cncfperiod  43141
  Copyright terms: Public domain W3C validator