Theorem ssrab2 3240

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

Syntax hints:   /\ wa 104   e. wcel 2148   {cab 2163   {crab 2459   C_ wss 3129

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3135  df-ss 3142

This theorem is referenced by:  ssrab3  3241  ssrabeq  3242  ifssun  3548  rabexg  4146  pwnss  4159  undifexmid  4193  exmidexmid  4196  exmidsssnc  4203  onintrab2im  4517  ordtriexmidlem  4518  ontr2exmid  4524  ordtri2or2exmidlem  4525  onsucsssucexmid  4526  onsucelsucexmidlem  4528  tfis  4582  nnregexmid  4620  dmmptss  5125  ssimaex  5577  f1oresrab  5681  canth  5828  riotacl  5844  pmvalg  6658  ssfiexmid  6875  domfiexmid  6877  ctssdccl  7109  ctssexmid  7147  genpelxp  7509  ltexprlempr  7606  cauappcvgprlemcl  7651  cauappcvgprlemladd  7656  caucvgprlemcl  7674  caucvgprprlemcl  7702  suplocexprlemex  7720  uzf  9530  supminfex  9596  rpre  9659  ixxf  9897  fzf  10011  expcl2lemap  10531  expclzaplem  10543  expge0  10555  expge1  10556  dvdsflip  11856  infssuzex  11949  infssuzcldc  11951  zsupssdc  11954  gcddvds  11963  uzwodc  12037  nnwosdc  12039  lcmn0cl  12067  phicl2  12213  phimullem  12224  eulerthlemfi  12227  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  phisum  12239  pcpremul  12292  ennnfonelemg  12403  ennnfonelemh  12404  ctiunctlemuom  12436  issubmd  12864  mhmeql  12875  epttop  13560  neipsm  13624  cnpfval  13665  blfvalps  13855  blfps  13879  blf  13880  divcnap  14025  cdivcncfap  14057  cnopnap  14064  ivthinclemex  14090  limcdifap  14101  dvfgg  14127  dvidlemap  14130  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvrecap  14147  lgsfcl  14379  lgscl  14385  bdrabexg  14628  subctctexmid  14720