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  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  11002  expclzaplem  11014  expge0  11026  expge1  11027  dvdsflip  12636  bitsf  12731  bitsfzolem  12739  gcddvds  12758  uzwodc  12832  nnwosdc  12834  nninfctlemfo  12835  lcmn0cl  12864  phicl2  13014  phimullem  13025  eulerthlemfi  13028  eulerthlemrprm  13029  eulerthlema  13030  eulerthlemh  13031  eulerthlemth  13032  phisum  13041  pcpremul  13094  ballotfilem2  13279  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemiex  13295  ballotfilem7  13330  ballotfilemth  13332  ennnfonelemg  13345  ennnfonelemh  13346  ctiunctlemuom  13378  issubmd  13832  mhmeql  13850  lspf  14777  asplss  15067  aspsubrg  15069  mplbascoe  15134  mplbasss  15139  epttop  15243  neipsm  15307  cnpfval  15348  blfvalps  15538  blfps  15562  blf  15563  divcnap  15718  cdivcncfap  15757  cnopnap  15764  ivthinclemex  15795  limcdifap  15815  dvfgg  15841  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvcnp2cntop  15852  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvrecap  15866  pellexlem3  16153  efnnfsumcl  16161  sgmval2  16175  efchtqdvds  16187  sgmmul  16212  ppiqub  16215  perfectlem2  16222  lgsfcl  16249  lgscl  16255  lgsquadlem1  16318  lgsquadlem2  16319  incistruhgr  16453  upgrss  16462  usgrss  16540  ushgredgedg  16589  ushgredgedgloop  16591  vtxdfifiun  16660  bdrabexg  17054  pw1map  17147  subctctexmid  17152  stnot  17161  wexmiddc  17164