Theorem ssrab2 3182

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

Syntax hints:   /\ wa 103   e. wcel 1480   {cab 2125   {crab 2420   C_ wss 3071

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rab 2425  df-in 3077  df-ss 3084

This theorem is referenced by:  ssrabeq  3183  rabexg  4071  pwnss  4083  undifexmid  4117  exmidexmid  4120  exmidsssnc  4126  onintrab2im  4434  ordtriexmidlem  4435  ontr2exmid  4440  ordtri2or2exmidlem  4441  onsucsssucexmid  4442  onsucelsucexmidlem  4444  tfis  4497  nnregexmid  4534  dmmptss  5035  ssimaex  5482  f1oresrab  5585  riotacl  5744  pmvalg  6553  ssfiexmid  6770  domfiexmid  6772  ctssdccl  6996  ctssexmid  7024  genpelxp  7319  ltexprlempr  7416  cauappcvgprlemcl  7461  cauappcvgprlemladd  7466  caucvgprlemcl  7484  caucvgprprlemcl  7512  suplocexprlemex  7530  uzf  9329  supminfex  9392  rpre  9448  ixxf  9681  fzf  9794  expcl2lemap  10305  expclzaplem  10317  expge0  10329  expge1  10330  dvdsflip  11549  infssuzex  11642  infssuzcldc  11644  gcddvds  11652  lcmn0cl  11749  phicl2  11890  phimullem  11901  ennnfonelemg  11916  ennnfonelemh  11917  ctiunctlemuom  11949  epttop  12259  neipsm  12323  cnpfval  12364  blfvalps  12554  blfps  12578  blf  12579  divcnap  12724  cdivcncfap  12756  cnopnap  12763  ivthinclemex  12789  limcdifap  12800  dvfgg  12826  dvidlemap  12829  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvrecap  12846  bdrabexg  13104  subctctexmid  13196