Theorem ssrab2 3309

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 2517	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		ssab2 3308	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
3	1, 2	eqsstri 3256	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   ∧ wa 104   ∈ wcel 2200  {cab 2215  {crab 2512   ⊆ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210

This theorem is referenced by:  ssrab3  3310  ssrabeq  3311  ifssun  3617  rabexg  4226  pwnss  4242  undifexmid  4276  exmidexmid  4279  exmidsssnc  4286  onintrab2im  4607  ordtriexmidlem  4608  ontr2exmid  4614  ordtri2or2exmidlem  4615  onsucsssucexmid  4616  onsucelsucexmidlem  4618  tfis  4672  nnregexmid  4710  dmmptss  5221  ssimaex  5688  f1oresrab  5793  canth  5945  riotacl  5963  pmvalg  6796  ssfiexmid  7026  domfiexmid  7028  ctssdccl  7266  ctssexmid  7305  genpelxp  7686  ltexprlempr  7783  cauappcvgprlemcl  7828  cauappcvgprlemladd  7833  caucvgprlemcl  7851  caucvgprprlemcl  7879  suplocexprlemex  7897  uzf  9713  supminfex  9780  rpre  9844  ixxf  10082  fzf  10196  infssuzex  10440  infssuzcldc  10442  zsupssdc  10445  expcl2lemap  10760  expclzaplem  10772  expge0  10784  expge1  10785  dvdsflip  12348  bitsf  12443  bitsfzolem  12451  gcddvds  12470  uzwodc  12544  nnwosdc  12546  nninfctlemfo  12547  lcmn0cl  12576  phicl2  12722  phimullem  12733  eulerthlemfi  12736  eulerthlemrprm  12737  eulerthlema  12738  eulerthlemh  12739  eulerthlemth  12740  phisum  12749  pcpremul  12802  ennnfonelemg  12960  ennnfonelemh  12961  ctiunctlemuom  12993  issubmd  13493  mhmeql  13511  lspf  14338  mplbascoe  14640  mplbasss  14645  epttop  14749  neipsm  14813  cnpfval  14854  blfvalps  15044  blfps  15068  blf  15069  divcnap  15224  cdivcncfap  15263  cnopnap  15270  ivthinclemex  15301  limcdifap  15321  dvfgg  15347  dvidlemap  15350  dvidrelem  15351  dvidsslem  15352  dvcnp2cntop  15358  dvaddxxbr  15360  dvmulxxbr  15361  dvcoapbr  15366  dvrecap  15372  sgmval2  15643  sgmmul  15655  perfectlem2  15659  lgsfcl  15672  lgscl  15678  lgsquadlem1  15741  lgsquadlem2  15742  incistruhgr  15875  upgrss  15884  usgrss  15960  ushgredgedg  16009  ushgredgedgloop  16011  bdrabexg  16199  2omap  16290  pw1map  16292  subctctexmid  16297