Theorem ssrab2 3313

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

Syntax hints:   /\ wa 104   e. wcel 2202   {cab 2217   {crab 2515   C_ wss 3201

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-in 3207  df-ss 3214

This theorem is referenced by:  ssrab3  3314  ssrabeq  3316  ifssun  3624  rabexg  4238  pwnss  4255  undifexmid  4289  exmidexmid  4292  exmidsssnc  4299  onintrab2im  4622  ordtriexmidlem  4623  ontr2exmid  4629  ordtri2or2exmidlem  4630  onsucsssucexmid  4631  onsucelsucexmidlem  4633  tfis  4687  nnregexmid  4725  dmmptss  5240  ssimaex  5716  f1oresrab  5820  canth  5979  riotacl  5997  suppssdmg  6427  pmvalg  6871  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  ctssdccl  7370  ctssexmid  7409  genpelxp  7791  ltexprlempr  7888  cauappcvgprlemcl  7933  cauappcvgprlemladd  7938  caucvgprlemcl  7956  caucvgprprlemcl  7984  suplocexprlemex  8002  uzf  9819  supminfex  9892  rpre  9956  ixxf  10194  fzf  10309  infssuzex  10556  infssuzcldc  10558  zsupssdc  10561  expcl2lemap  10876  expclzaplem  10888  expge0  10900  expge1  10901  dvdsflip  12492  bitsf  12587  bitsfzolem  12595  gcddvds  12614  uzwodc  12688  nnwosdc  12690  nninfctlemfo  12691  lcmn0cl  12720  phicl2  12866  phimullem  12877  eulerthlemfi  12880  eulerthlemrprm  12881  eulerthlema  12882  eulerthlemh  12883  eulerthlemth  12884  phisum  12893  pcpremul  12946  ennnfonelemg  13104  ennnfonelemh  13105  ctiunctlemuom  13137  issubmd  13637  mhmeql  13655  lspf  14485  mplbascoe  14792  mplbasss  14797  epttop  14901  neipsm  14965  cnpfval  15006  blfvalps  15196  blfps  15220  blf  15221  divcnap  15376  cdivcncfap  15415  cnopnap  15422  ivthinclemex  15453  limcdifap  15473  dvfgg  15499  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvaddxxbr  15512  dvmulxxbr  15513  dvcoapbr  15518  dvrecap  15524  pellexlem3  15793  sgmval2  15798  sgmmul  15810  perfectlem2  15814  lgsfcl  15827  lgscl  15833  lgsquadlem1  15896  lgsquadlem2  15897  incistruhgr  16031  upgrss  16040  usgrss  16118  ushgredgedg  16167  ushgredgedgloop  16169  vtxdfifiun  16238  bdrabexg  16622  2omap  16715  pw1map  16717  subctctexmid  16722