ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssrab2 Unicode version

Theorem ssrab2 3186
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
ssrab2  |-  { x  e.  A  |  ph }  C_  A
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem ssrab2
StepHypRef Expression
1 df-rab 2426 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3185 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3133 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 103    e. wcel 1481   {cab 2126   {crab 2421    C_ wss 3075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-in 3081  df-ss 3088
This theorem is referenced by:  ssrabeq  3187  rabexg  4078  pwnss  4090  undifexmid  4124  exmidexmid  4127  exmidsssnc  4133  onintrab2im  4441  ordtriexmidlem  4442  ontr2exmid  4447  ordtri2or2exmidlem  4448  onsucsssucexmid  4449  onsucelsucexmidlem  4451  tfis  4504  nnregexmid  4541  dmmptss  5042  ssimaex  5489  f1oresrab  5592  riotacl  5751  pmvalg  6560  ssfiexmid  6777  domfiexmid  6779  ctssdccl  7003  ctssexmid  7031  genpelxp  7342  ltexprlempr  7439  cauappcvgprlemcl  7484  cauappcvgprlemladd  7489  caucvgprlemcl  7507  caucvgprprlemcl  7535  suplocexprlemex  7553  uzf  9352  supminfex  9418  rpre  9476  ixxf  9710  fzf  9824  expcl2lemap  10335  expclzaplem  10347  expge0  10359  expge1  10360  dvdsflip  11583  infssuzex  11676  infssuzcldc  11678  gcddvds  11686  lcmn0cl  11783  phicl2  11924  phimullem  11935  ennnfonelemg  11950  ennnfonelemh  11951  ctiunctlemuom  11983  epttop  12296  neipsm  12360  cnpfval  12401  blfvalps  12591  blfps  12615  blf  12616  divcnap  12761  cdivcncfap  12793  cnopnap  12800  ivthinclemex  12826  limcdifap  12837  dvfgg  12863  dvidlemap  12866  dvcnp2cntop  12869  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  dvrecap  12883  bdrabexg  13273  subctctexmid  13367
  Copyright terms: Public domain W3C validator