Theorem ssrab2 3333

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)

Assertion

Ref	Expression
ssrab2	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab2

Step	Hyp	Ref	Expression
1		df-rab 2537	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		ssab2 3332	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
3	1, 2	eqsstri 3280	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   ∧ wa 104   ∈ wcel 2209  {cab 2224  {crab 2532   ⊆ wss 3220

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 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 theorem 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 referenced by:  ssrab3  3334  ssrabeq  3336  ifssun  3655  rabexg  4277  pwnss  4294  undifexmid  4328  exmidexmid  4331  exmidsssnc  4338  onintrab2im  4663  ordtriexmidlem  4664  ontr2exmid  4670  ordtri2or2exmidlem  4671  onsucsssucexmid  4672  onsucelsucexmidlem  4674  tfis  4728  nnregexmid  4766  dmmptss  5282  ssimaex  5761  f1oresrab  5867  canth  6030  riotacl  6048  suppssdmg  6483  pmvalg  6927  ssfiexmid  7172  ssfiexmidt  7174  domfiexmid  7176  2omap  7312  ctssdccl  7445  ctssexmid  7484  genpelxp  7872  ltexprlempr  7969  cauappcvgprlemcl  8014  cauappcvgprlemladd  8019  caucvgprlemcl  8037  caucvgprprlemcl  8065  suplocexprlemex  8083  uzf  9907  supminfex  9980  rpre  10044  ixxf  10283  fzf  10398  infssuzex  10649  infssuzcldc  10651  zsupssdc  10656  expcl2lemap  10971  expclzaplem  10983  expge0  10995  expge1  10996  dvdsflip  12601  bitsf  12696  bitsfzolem  12704  gcddvds  12723  uzwodc  12797  nnwosdc  12799  nninfctlemfo  12800  lcmn0cl  12829  phicl2  12975  phimullem  12986  eulerthlemfi  12989  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemh  12992  eulerthlemth  12993  phisum  13002  pcpremul  13055  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemiex  13227  ballotfilem7  13262  ballotfilemth  13264  ennnfonelemg  13277  ennnfonelemh  13278  ctiunctlemuom  13310  issubmd  13764  mhmeql  13782  lspf  14709  asplss  14999  aspsubrg  15001  mplbascoe  15065  mplbasss  15070  epttop  15174  neipsm  15238  cnpfval  15279  blfvalps  15469  blfps  15493  blf  15494  divcnap  15649  cdivcncfap  15688  cnopnap  15695  ivthinclemex  15726  limcdifap  15746  dvfgg  15772  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvcnp2cntop  15783  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvrecap  15797  pellexlem3  16076  sgmval2  16081  sgmmul  16093  perfectlem2  16097  lgsfcl  16110  lgscl  16116  lgsquadlem1  16179  lgsquadlem2  16180  incistruhgr  16314  upgrss  16323  usgrss  16401  ushgredgedg  16450  ushgredgedgloop  16452  vtxdfifiun  16521  bdrabexg  16915  pw1map  17008  subctctexmid  17013