Theorem ssrab2 3255

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

Syntax hints:   /\ wa 104   e. wcel 2160   {cab 2175   {crab 2472   C_ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rab 2477  df-in 3150  df-ss 3157

This theorem is referenced by:  ssrab3  3256  ssrabeq  3257  ifssun  3563  rabexg  4161  pwnss  4174  undifexmid  4208  exmidexmid  4211  exmidsssnc  4218  onintrab2im  4532  ordtriexmidlem  4533  ontr2exmid  4539  ordtri2or2exmidlem  4540  onsucsssucexmid  4541  onsucelsucexmidlem  4543  tfis  4597  nnregexmid  4635  dmmptss  5140  ssimaex  5594  f1oresrab  5698  canth  5846  riotacl  5862  pmvalg  6680  ssfiexmid  6899  domfiexmid  6901  ctssdccl  7135  ctssexmid  7173  genpelxp  7535  ltexprlempr  7632  cauappcvgprlemcl  7677  cauappcvgprlemladd  7682  caucvgprlemcl  7700  caucvgprprlemcl  7728  suplocexprlemex  7746  uzf  9556  supminfex  9622  rpre  9685  ixxf  9923  fzf  10037  expcl2lemap  10558  expclzaplem  10570  expge0  10582  expge1  10583  dvdsflip  11884  infssuzex  11977  infssuzcldc  11979  zsupssdc  11982  gcddvds  11991  uzwodc  12065  nnwosdc  12067  lcmn0cl  12095  phicl2  12241  phimullem  12252  eulerthlemfi  12255  eulerthlemrprm  12256  eulerthlema  12257  eulerthlemh  12258  eulerthlemth  12259  phisum  12267  pcpremul  12320  ennnfonelemg  12449  ennnfonelemh  12450  ctiunctlemuom  12482  issubmd  12919  mhmeql  12937  lspf  13698  epttop  14027  neipsm  14091  cnpfval  14132  blfvalps  14322  blfps  14346  blf  14347  divcnap  14492  cdivcncfap  14524  cnopnap  14531  ivthinclemex  14557  limcdifap  14568  dvfgg  14594  dvidlemap  14597  dvcnp2cntop  14600  dvaddxxbr  14602  dvmulxxbr  14603  dvcoapbr  14608  dvrecap  14614  lgsfcl  14846  lgscl  14852  bdrabexg  15095  subctctexmid  15188