Theorem ssrab2 3309

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

Syntax hints:   /\ wa 104   e. wcel 2200   {cab 2215   {crab 2512   C_ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210

This theorem is referenced by:  ssrab3  3310  ssrabeq  3311  ifssun  3617  rabexg  4227  pwnss  4243  undifexmid  4277  exmidexmid  4280  exmidsssnc  4287  onintrab2im  4610  ordtriexmidlem  4611  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  onsucelsucexmidlem  4621  tfis  4675  nnregexmid  4713  dmmptss  5225  ssimaex  5697  f1oresrab  5802  canth  5958  riotacl  5976  pmvalg  6814  ssfiexmid  7046  domfiexmid  7048  ctssdccl  7289  ctssexmid  7328  genpelxp  7709  ltexprlempr  7806  cauappcvgprlemcl  7851  cauappcvgprlemladd  7856  caucvgprlemcl  7874  caucvgprprlemcl  7902  suplocexprlemex  7920  uzf  9736  supminfex  9804  rpre  9868  ixxf  10106  fzf  10220  infssuzex  10465  infssuzcldc  10467  zsupssdc  10470  expcl2lemap  10785  expclzaplem  10797  expge0  10809  expge1  10810  dvdsflip  12378  bitsf  12473  bitsfzolem  12481  gcddvds  12500  uzwodc  12574  nnwosdc  12576  nninfctlemfo  12577  lcmn0cl  12606  phicl2  12752  phimullem  12763  eulerthlemfi  12766  eulerthlemrprm  12767  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  phisum  12779  pcpremul  12832  ennnfonelemg  12990  ennnfonelemh  12991  ctiunctlemuom  13023  issubmd  13523  mhmeql  13541  lspf  14369  mplbascoe  14671  mplbasss  14676  epttop  14780  neipsm  14844  cnpfval  14885  blfvalps  15075  blfps  15099  blf  15100  divcnap  15255  cdivcncfap  15294  cnopnap  15301  ivthinclemex  15332  limcdifap  15352  dvfgg  15378  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvrecap  15403  sgmval2  15674  sgmmul  15686  perfectlem2  15690  lgsfcl  15703  lgscl  15709  lgsquadlem1  15772  lgsquadlem2  15773  incistruhgr  15906  upgrss  15915  usgrss  15991  ushgredgedg  16040  ushgredgedgloop  16042  vtxdfifiun  16057  bdrabexg  16352  2omap  16446  pw1map  16448  subctctexmid  16453