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

Theorem ssrab3 4054
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 4053 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
31, 2eqsstri 3998 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  {crab 3139  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940  df-ss 3949
This theorem is referenced by:  dmmptss  6088  omsson  7573  oawordeulem  8169  ordtypelem2  8971  wemapso2lem  9004  wemapwe  9148  cplem1  9306  cofsmo  9679  fin23lem28  9750  fin23lem30  9752  isf32lem5  9767  isf32lem6  9768  isf32lem7  9769  isf32lem8  9770  hsmexlem4  9839  hsmexlem5  9840  hsmexlem6  9841  zorn2lem1  9906  zorn2lem3  9908  zorn2lem4  9909  zorn2lem5  9910  0nnq  10334  elpqn  10335  rpnnen1lem2  12364  rpssre  12384  sqrlem5  14594  dvdsflip  15655  divalglem2  15734  divalglem5  15736  divalglem8  15739  gcdcllem3  15838  bezoutlem2  15876  bezoutlem3  15877  maxprmfct  16041  phimullem  16104  eulerthlem2  16107  pclem  16163  infpn2  16237  prmreclem2  16241  prmreclem3  16242  prmreclem5  16244  4sqlem13  16281  4sqlem14  16282  4sqlem17  16285  4sqlem18  16286  vdwnnlem3  16321  ramcl2lem  16333  ramtcl  16334  ramtcl2  16335  ramtub  16336  imasdsval2  16777  gsumval1  17881  nmzsubg  18255  nmznsg  18258  conjnmz  18330  conjnmzb  18331  gastacl  18377  sylow1lem2  18653  sylow1lem3  18654  sylow1lem4  18655  sylow1lem5  18656  sylow2a  18673  sylow3lem2  18682  ablfacrplem  19116  ablfacrp2  19118  ablfac1eu  19124  pgpfaclem1  19132  ablfaclem2  19137  ablfaclem3  19138  lspsolvlem  19843  lbsextlem2  19860  lbsextlem3  19861  lbsextlem4  19862  rrgeq0  19991  rrgss  19993  psrbagconf1o  20082  psrass1lem  20085  mplbasss  20140  coe1mul2lem2  20364  cygznlem2a  20642  psgnghm  20652  dsmmbase  20807  frlmsslsp  20868  mretopd  21628  hauscmplem  21942  ptcmplem1  22588  ptcmplem3  22590  tgpconncompeqg  22647  imasdsf1olem  22910  blcld  23042  icccmplem1  23357  icccmplem2  23358  icccmplem3  23359  rrxf  23931  ivthlem1  23979  ivthlem2  23980  ivthlem3  23981  ovolsslem  24012  ovolicc2lem3  24047  ovolicc2lem4  24048  ovolicc2lem5  24049  ovolicc2  24050  dyadmbllem  24127  dyadmbl  24128  iblmbf  24295  abelthlem4  24949  abelthlem6  24951  abelthlem9  24955  abelth  24956  dvatan  25440  atancn  25441  lgamucov  25542  lgamucov2  25543  ftalem3  25579  dvdsmulf1o  25698  fsumdvdsmul  25699  lgsfcl2  25806  rpvmasum2  26015  dchrisum0re  26016  dchrisum0lema  26017  dchrisum0lem1b  26018  dchrisum0lem1  26019  dchrisum0lem2a  26020  dchrisum0lem2  26021  dchrisum0lem3  26022  dchrisum0  26023  pntlem3  26112  axcontlem2  26678  axcontlem7  26683  axcontlem8  26684  axcontlem10  26686  upgrreslem  27013  umgrreslem  27014  usgrres  27017  vtxdginducedm1lem2  27249  finsumvtxdg2ssteplem1  27254  clwwlksswrd  27692  frgrwopregbsn  28023  frgrwopreg1  28024  atssch  30047  eulerpartlemgvv  31533  reprpmtf1o  31796  hgt750lemb  31826  hgt750leme  31828  bnj1212  31970  bnj213  32053  bnj1286  32188  bnj1312  32227  bnj1523  32240  wlimss  33013  bj-cmnssmnd  34442  bj-grpssmnd  34444  fglmod  39551  scottss  40456  limcperiod  41785  cncfshift  42033  cncfperiod  42038
  Copyright terms: Public domain W3C validator