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

Theorem ssrab2 3152
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 2402 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3151 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3099 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 103    e. wcel 1465   {cab 2103   {crab 2397    C_ wss 3041
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rab 2402  df-in 3047  df-ss 3054
This theorem is referenced by:  ssrabeq  3153  rabexg  4041  pwnss  4053  undifexmid  4087  exmidexmid  4090  exmidsssnc  4096  onintrab2im  4404  ordtriexmidlem  4405  ontr2exmid  4410  ordtri2or2exmidlem  4411  onsucsssucexmid  4412  onsucelsucexmidlem  4414  tfis  4467  nnregexmid  4504  dmmptss  5005  ssimaex  5450  f1oresrab  5553  riotacl  5712  pmvalg  6521  ssfiexmid  6738  domfiexmid  6740  ctssdccl  6964  ctssexmid  6992  genpelxp  7287  ltexprlempr  7384  cauappcvgprlemcl  7429  cauappcvgprlemladd  7434  caucvgprlemcl  7452  caucvgprprlemcl  7480  suplocexprlemex  7498  uzf  9297  supminfex  9360  rpre  9416  ixxf  9649  fzf  9762  expcl2lemap  10273  expclzaplem  10285  expge0  10297  expge1  10298  dvdsflip  11476  infssuzex  11569  infssuzcldc  11571  gcddvds  11579  lcmn0cl  11676  phicl2  11817  phimullem  11828  ennnfonelemg  11843  ennnfonelemh  11844  ctiunctlemuom  11876  epttop  12186  neipsm  12250  cnpfval  12291  blfvalps  12481  blfps  12505  blf  12506  divcnap  12651  cdivcncfap  12683  cnopnap  12690  ivthinclemex  12716  limcdifap  12727  dvfgg  12753  dvidlemap  12756  dvcnp2cntop  12759  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvrecap  12773  bdrabexg  13031  subctctexmid  13123
  Copyright terms: Public domain W3C validator