Theorem ssrab2 3333

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

This proof depends on syntax axioms:   /\ wa 104   e. wcel 2209   {cab 2224   {crab 2532   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233

This theorem is used by:  ssrab3  3334  ssrabeq  3336  ifssun  3655  rabexg  4279  pwnss  4296  undifexmid  4330  exmidexmid  4333  exmidsssnc  4340  onintrab2im  4665  ordtriexmidlem  4666  ontr2exmid  4672  ordtri2or2exmidlem  4673  onsucsssucexmid  4674  onsucelsucexmidlem  4676  tfis  4730  nnregexmid  4768  dmmptss  5284  ssimaex  5764  f1oresrab  5873  canth  6036  riotacl  6054  suppssdmg  6489  pmvalg  6933  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  2omap  7319  ctssdccl  7452  ctssexmid  7491  genpelxp  7879  ltexprlempr  7976  cauappcvgprlemcl  8021  cauappcvgprlemladd  8026  caucvgprlemcl  8044  caucvgprprlemcl  8072  suplocexprlemex  8090  uzf  9934  supminfex  10007  rpre  10072  ixxf  10311  fzf  10426  infssuzex  10677  infssuzcldc  10679  zsupssdc  10684  expcl2lemap  11003  expclzaplem  11015  expge0  11027  expge1  11028  dvdsflip  12637  bitsf  12732  bitsfzolem  12740  gcddvds  12759  uzwodc  12833  nnwosdc  12835  nninfctlemfo  12836  lcmn0cl  12865  phicl2  13015  phimullem  13026  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  phisum  13042  pcpremul  13095  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemiex  13296  ballotfilem7  13331  ballotfilemth  13333  ennnfonelemg  13346  ennnfonelemh  13347  ctiunctlemuom  13379  issubmd  13834  mhmeql  13852  cntzssv  14154  lspf  14810  asplss  15100  aspsubrg  15102  mplbascoe  15173  mplbasss  15178  epttop  15282  neipsm  15346  cnpfval  15387  blfvalps  15577  blfps  15601  blf  15602  divcnap  15757  cdivcncfap  15796  cnopnap  15803  ivthinclemex  15834  limcdifap  15854  dvfgg  15880  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvrecap  15905  pellexlem3  16192  efnnfsumcl  16200  sgmval2  16214  efchtqdvds  16226  sgmmul  16251  ppiqub  16254  perfectlem2  16261  lgsfcl  16293  lgscl  16299  lgsquadlem1  16362  lgsquadlem2  16363  incistruhgr  16497  upgrss  16506  usgrss  16584  ushgredgedg  16633  ushgredgedgloop  16635  vtxdfifiun  16704  bdrabexg  17098  pw1map  17191  subctctexmid  17196  stnot  17205  wexmiddc  17208