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

Theorem ssrab3 4032
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 4031 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
31, 2eqsstri 3976 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  {crab 3134  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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-in 3915  df-ss 3925
This theorem is referenced by:  dmmptss  6073  omsson  7569  oawordeulem  8167  ordtypelem2  8971  wemapso2lem  9004  wemapwe  9148  cplem1  9306  cofsmo  9680  fin23lem28  9751  fin23lem30  9753  isf32lem5  9768  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  hsmexlem4  9840  hsmexlem5  9841  hsmexlem6  9842  zorn2lem1  9907  zorn2lem3  9909  zorn2lem4  9910  zorn2lem5  9911  0nnq  10335  elpqn  10336  rpnnen1lem2  12364  rpssre  12384  sqrlem5  14597  dvdsflip  15658  divalglem2  15735  divalglem5  15737  divalglem8  15740  gcdcllem3  15839  bezoutlem2  15877  bezoutlem3  15878  maxprmfct  16042  phimullem  16105  eulerthlem2  16108  pclem  16164  infpn2  16238  prmreclem2  16242  prmreclem3  16243  prmreclem5  16245  4sqlem13  16282  4sqlem14  16283  4sqlem17  16286  4sqlem18  16287  vdwnnlem3  16322  ramcl2lem  16334  ramtcl  16335  ramtcl2  16336  ramtub  16337  imasdsval2  16780  gsumval1  17884  nmzsubg  18308  nmznsg  18311  conjnmz  18383  conjnmzb  18384  gastacl  18430  sylow1lem2  18715  sylow1lem3  18716  sylow1lem4  18717  sylow1lem5  18718  sylow2a  18735  sylow3lem2  18744  ablfacrplem  19178  ablfacrp2  19180  ablfac1eu  19186  pgpfaclem1  19194  ablfaclem2  19199  ablfaclem3  19200  lspsolvlem  19905  lbsextlem2  19922  lbsextlem3  19923  lbsextlem4  19924  rrgeq0  20054  rrgss  20056  cygznlem2a  20257  psgnghm  20267  dsmmbase  20422  frlmsslsp  20483  psrbagconf1o  20610  psrass1lem  20613  mplbasss  20668  coe1mul2lem2  20895  mretopd  21695  hauscmplem  22009  ptcmplem1  22655  ptcmplem3  22657  tgpconncompeqg  22715  imasdsf1olem  22978  blcld  23110  icccmplem1  23425  icccmplem2  23426  icccmplem3  23427  rrxf  24003  ivthlem1  24053  ivthlem2  24054  ivthlem3  24055  ovolsslem  24086  ovolicc2lem3  24121  ovolicc2lem4  24122  ovolicc2lem5  24123  ovolicc2  24124  dyadmbllem  24201  dyadmbl  24202  iblmbf  24369  abelthlem4  25027  abelthlem6  25029  abelthlem9  25033  abelth  25034  dvatan  25519  atancn  25520  lgamucov  25621  lgamucov2  25622  ftalem3  25658  dvdsmulf1o  25777  fsumdvdsmul  25778  lgsfcl2  25885  rpvmasum2  26094  dchrisum0re  26095  dchrisum0lema  26096  dchrisum0lem1b  26097  dchrisum0lem1  26098  dchrisum0lem2a  26099  dchrisum0lem2  26100  dchrisum0lem3  26101  dchrisum0  26102  pntlem3  26191  axcontlem2  26757  axcontlem7  26762  axcontlem8  26763  axcontlem10  26765  upgrreslem  27092  umgrreslem  27093  usgrres  27096  vtxdginducedm1lem2  27328  finsumvtxdg2ssteplem1  27333  clwwlksswrd  27770  frgrwopregbsn  28100  frgrwopreg1  28101  atssch  30124  ssmxidllem  31020  eulerpartlemgvv  31708  reprpmtf1o  31971  hgt750lemb  32001  hgt750leme  32003  bnj1212  32145  bnj213  32228  bnj1286  32365  bnj1312  32404  bnj1523  32417  wlimss  33190  bj-smgrpssmgm  34644  bj-mndsssmgrp  34646  bj-cmnssmnd  34648  bj-grpssmnd  34650  fglmod  39947  scottss  40885  limcperiod  42209  cncfshift  42455  cncfperiod  42460
  Copyright terms: Public domain W3C validator