Theorem ssrab2 3269

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 3268	. 2 |- { x | ( x e. A /\ ph ) } C_ A
3	1, 2	eqsstri 3216	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  3270  ssrabeq  3271  ifssun  3576  rabexg  4177  pwnss  4193  undifexmid  4227  exmidexmid  4230  exmidsssnc  4237  onintrab2im  4555  ordtriexmidlem  4556  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucsssucexmid  4564  onsucelsucexmidlem  4566  tfis  4620  nnregexmid  4658  dmmptss  5167  ssimaex  5625  f1oresrab  5730  canth  5878  riotacl  5895  pmvalg  6727  ssfiexmid  6946  domfiexmid  6948  ctssdccl  7186  ctssexmid  7225  genpelxp  7597  ltexprlempr  7694  cauappcvgprlemcl  7739  cauappcvgprlemladd  7744  caucvgprlemcl  7762  caucvgprprlemcl  7790  suplocexprlemex  7808  uzf  9623  supminfex  9690  rpre  9754  ixxf  9992  fzf  10106  infssuzex  10342  infssuzcldc  10344  zsupssdc  10347  expcl2lemap  10662  expclzaplem  10674  expge0  10686  expge1  10687  dvdsflip  12035  bitsf  12130  bitsfzolem  12138  gcddvds  12157  uzwodc  12231  nnwosdc  12233  nninfctlemfo  12234  lcmn0cl  12263  phicl2  12409  phimullem  12420  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  phisum  12436  pcpremul  12489  ennnfonelemg  12647  ennnfonelemh  12648  ctiunctlemuom  12680  issubmd  13178  mhmeql  13196  lspf  14023  mplbascoe  14325  mplbasss  14330  epttop  14434  neipsm  14498  cnpfval  14539  blfvalps  14729  blfps  14753  blf  14754  divcnap  14909  cdivcncfap  14948  cnopnap  14955  ivthinclemex  14986  limcdifap  15006  dvfgg  15032  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvrecap  15057  sgmval2  15328  sgmmul  15340  perfectlem2  15344  lgsfcl  15357  lgscl  15363  lgsquadlem1  15426  lgsquadlem2  15427  bdrabexg  15660  2omap  15750  subctctexmid  15755