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 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

This proof depends on syntax axioms:   ∧ wa 104   ∈ wcel 2209  {cab 2224  {crab 2532   ⊆ 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  7318  ctssdccl  7451  ctssexmid  7490  genpelxp  7878  ltexprlempr  7975  cauappcvgprlemcl  8020  cauappcvgprlemladd  8025  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocexprlemex  8089  uzf  9926  supminfex  9999  rpre  10063  ixxf  10302  fzf  10417  infssuzex  10668  infssuzcldc  10670  zsupssdc  10675  expcl2lemap  10990  expclzaplem  11002  expge0  11014  expge1  11015  dvdsflip  12620  bitsf  12715  bitsfzolem  12723  gcddvds  12742  uzwodc  12816  nnwosdc  12818  nninfctlemfo  12819  lcmn0cl  12848  phicl2  12994  phimullem  13005  eulerthlemfi  13008  eulerthlemrprm  13009  eulerthlema  13010  eulerthlemh  13011  eulerthlemth  13012  phisum  13021  pcpremul  13074  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemiex  13246  ballotfilem7  13281  ballotfilemth  13283  ennnfonelemg  13296  ennnfonelemh  13297  ctiunctlemuom  13329  issubmd  13783  mhmeql  13801  lspf  14728  asplss  15018  aspsubrg  15020  mplbascoe  15084  mplbasss  15089  epttop  15193  neipsm  15257  cnpfval  15298  blfvalps  15488  blfps  15512  blf  15513  divcnap  15668  cdivcncfap  15707  cnopnap  15714  ivthinclemex  15745  limcdifap  15765  dvfgg  15791  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvcnp2cntop  15802  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvrecap  15816  pellexlem3  16099  sgmval2  16104  sgmmul  16116  perfectlem2  16120  lgsfcl  16139  lgscl  16145  lgsquadlem1  16208  lgsquadlem2  16209  incistruhgr  16343  upgrss  16352  usgrss  16430  ushgredgedg  16479  ushgredgedgloop  16481  vtxdfifiun  16550  bdrabexg  16944  pw1map  17037  subctctexmid  17042  stnot  17051  wexmiddc  17054