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  4281  pwnss  4298  undifexmid  4332  exmidexmid  4335  exmidsssnc  4342  onintrab2im  4667  ordtriexmidlem  4668  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucsssucexmid  4676  onsucelsucexmidlem  4678  tfis  4732  nnregexmid  4770  dmmptss  5287  ssimaex  5767  f1oresrab  5876  canth  6039  riotacl  6057  suppssdmg  6493  pmvalg  6938  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  2omap  7325  ctssdccl  7458  ctssexmid  7497  genpelxp  7885  ltexprlempr  7982  cauappcvgprlemcl  8027  cauappcvgprlemladd  8032  caucvgprlemcl  8050  caucvgprprlemcl  8078  suplocexprlemex  8096  uzf  9940  supminfex  10013  rpre  10078  ixxf  10317  fzf  10432  infssuzex  10683  infssuzcldc  10685  zsupssdc  10690  expcl2lemap  11009  expclzaplem  11021  expge0  11033  expge1  11034  dvdsflip  12643  bitsf  12738  bitsfzolem  12746  gcddvds  12765  uzwodc  12839  nnwosdc  12841  nninfctlemfo  12842  lcmn0cl  12871  phicl2  13021  phimullem  13032  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  phisum  13048  pcpremul  13101  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemiex  13302  ballotfilem7  13337  ballotfilemth  13339  ennnfonelemg  13352  ennnfonelemh  13353  ctiunctlemuom  13385  issubmd  13840  mhmeql  13858  cntzssv  14160  lspf  14835  asplss  15125  aspsubrg  15127  psrbagmax  15190  psrbagfsuppd  15193  psrass1filem  15196  psrdifi  15222  psrdirfi  15223  mplbas  15235  epttop  15349  neipsm  15413  cnpfval  15454  blfvalps  15644  blfps  15668  blf  15669  divcnap  15824  cdivcncfap  15863  cnopnap  15870  ivthinclemex  15901  limcdifap  15921  dvfgg  15947  dvidlemap  15950  dvidrelem  15951  dvidsslem  15952  dvcnp2cntop  15958  dvaddxxbr  15960  dvmulxxbr  15961  dvcoapbr  15966  dvrecap  15972  pellexlem3  16264  efnnfsumcl  16272  sgmval2  16286  efchtqdvds  16298  sgmmul  16323  ppiqub  16326  perfectlem2  16333  lgsfcl  16365  lgscl  16371  lgsquadlem1  16434  lgsquadlem2  16435  incistruhgr  16569  upgrss  16578  usgrss  16656  ushgredgedg  16705  ushgredgedgloop  16707  vtxdfifiun  16776  bdrabexg  17170  pw1map  17263  subctctexmid  17268  stnot  17277  wexmiddc  17280