Theorem ssrab2 3268

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

Step	Hyp	Ref	Expression
1		df-rab 2484	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		ssab2 3267	. 2 |- { x | ( x e. A /\ ph ) } C_ A
3	1, 2	eqsstri 3215	1 |- { x e. A | ph } C_ A

Syntax hints:   /\ wa 104   e. wcel 2167   {cab 2182   {crab 2479   C_ wss 3157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-in 3163  df-ss 3170

This theorem is referenced by:  ssrab3  3269  ssrabeq  3270  ifssun  3575  rabexg  4176  pwnss  4192  undifexmid  4226  exmidexmid  4229  exmidsssnc  4236  onintrab2im  4554  ordtriexmidlem  4555  ontr2exmid  4561  ordtri2or2exmidlem  4562  onsucsssucexmid  4563  onsucelsucexmidlem  4565  tfis  4619  nnregexmid  4657  dmmptss  5166  ssimaex  5622  f1oresrab  5727  canth  5875  riotacl  5892  pmvalg  6718  ssfiexmid  6937  domfiexmid  6939  ctssdccl  7177  ctssexmid  7216  genpelxp  7578  ltexprlempr  7675  cauappcvgprlemcl  7720  cauappcvgprlemladd  7725  caucvgprlemcl  7743  caucvgprprlemcl  7771  suplocexprlemex  7789  uzf  9604  supminfex  9671  rpre  9735  ixxf  9973  fzf  10087  infssuzex  10323  infssuzcldc  10325  zsupssdc  10328  expcl2lemap  10643  expclzaplem  10655  expge0  10667  expge1  10668  dvdsflip  12016  bitsf  12111  bitsfzolem  12118  gcddvds  12130  uzwodc  12204  nnwosdc  12206  nninfctlemfo  12207  lcmn0cl  12236  phicl2  12382  phimullem  12393  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  phisum  12409  pcpremul  12462  ennnfonelemg  12620  ennnfonelemh  12621  ctiunctlemuom  12653  issubmd  13106  mhmeql  13124  lspf  13945  epttop  14326  neipsm  14390  cnpfval  14431  blfvalps  14621  blfps  14645  blf  14646  divcnap  14801  cdivcncfap  14840  cnopnap  14847  ivthinclemex  14878  limcdifap  14898  dvfgg  14924  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvrecap  14949  sgmval2  15220  sgmmul  15232  perfectlem2  15236  lgsfcl  15249  lgscl  15255  lgsquadlem1  15318  lgsquadlem2  15319  bdrabexg  15552  subctctexmid  15645