Theorem ssrab2 3146

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 2397	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		ssab2 3145	. 2 |- { x | ( x e. A /\ ph ) } C_ A
3	1, 2	eqsstri 3093	1 |- { x e. A | ph } C_ A

Syntax hints:   /\ wa 103   e. wcel 1461   {cab 2099   {crab 2392   C_ wss 3035

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rab 2397  df-in 3041  df-ss 3048

This theorem is referenced by:  ssrabeq  3147  rabexg  4029  pwnss  4041  undifexmid  4075  exmidexmid  4078  exmidsssnc  4084  onintrab2im  4392  ordtriexmidlem  4393  ontr2exmid  4398  ordtri2or2exmidlem  4399  onsucsssucexmid  4400  onsucelsucexmidlem  4402  tfis  4455  nnregexmid  4492  dmmptss  4991  ssimaex  5434  f1oresrab  5537  riotacl  5696  pmvalg  6505  ssfiexmid  6721  domfiexmid  6723  ctssdccl  6946  ctssexmid  6972  genpelxp  7261  ltexprlempr  7358  cauappcvgprlemcl  7403  cauappcvgprlemladd  7408  caucvgprlemcl  7426  caucvgprprlemcl  7454  uzf  9225  supminfex  9288  rpre  9343  ixxf  9568  fzf  9681  expcl2lemap  10192  expclzaplem  10204  expge0  10216  expge1  10217  dvdsflip  11391  infssuzex  11484  infssuzcldc  11486  gcddvds  11494  lcmn0cl  11589  phicl2  11729  phimullem  11740  ennnfonelemg  11755  ennnfonelemh  11756  ctiunctlemuom  11786  epttop  12096  neipsm  12160  cnpfval  12201  blfvalps  12368  blfps  12392  blf  12393  divcnap  12535  cdivcncfap  12567  limcdifap  12581  dvfgg  12606  dvidlemap  12609  dvcnp2cntop  12612  dvaddxxbr  12614  bdrabexg  12787