Theorem ssrab2 3313

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

Syntax hints:   ∧ wa 104   ∈ wcel 2202  {cab 2217  {crab 2515   ⊆ wss 3201

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-in 3207  df-ss 3214

This theorem is referenced by:  ssrab3  3314  ssrabeq  3316  ifssun  3624  rabexg  4238  pwnss  4255  undifexmid  4289  exmidexmid  4292  exmidsssnc  4299  onintrab2im  4622  ordtriexmidlem  4623  ontr2exmid  4629  ordtri2or2exmidlem  4630  onsucsssucexmid  4631  onsucelsucexmidlem  4633  tfis  4687  nnregexmid  4725  dmmptss  5240  ssimaex  5716  f1oresrab  5820  canth  5979  riotacl  5997  suppssdmg  6427  pmvalg  6871  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  ctssdccl  7353  ctssexmid  7392  genpelxp  7774  ltexprlempr  7871  cauappcvgprlemcl  7916  cauappcvgprlemladd  7921  caucvgprlemcl  7939  caucvgprprlemcl  7967  suplocexprlemex  7985  uzf  9801  supminfex  9874  rpre  9938  ixxf  10176  fzf  10290  infssuzex  10537  infssuzcldc  10539  zsupssdc  10542  expcl2lemap  10857  expclzaplem  10869  expge0  10881  expge1  10882  dvdsflip  12473  bitsf  12568  bitsfzolem  12576  gcddvds  12595  uzwodc  12669  nnwosdc  12671  nninfctlemfo  12672  lcmn0cl  12701  phicl2  12847  phimullem  12858  eulerthlemfi  12861  eulerthlemrprm  12862  eulerthlema  12863  eulerthlemh  12864  eulerthlemth  12865  phisum  12874  pcpremul  12927  ennnfonelemg  13085  ennnfonelemh  13086  ctiunctlemuom  13118  issubmd  13618  mhmeql  13636  lspf  14465  mplbascoe  14772  mplbasss  14777  epttop  14881  neipsm  14945  cnpfval  14986  blfvalps  15176  blfps  15200  blf  15201  divcnap  15356  cdivcncfap  15395  cnopnap  15402  ivthinclemex  15433  limcdifap  15453  dvfgg  15479  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvcnp2cntop  15490  dvaddxxbr  15492  dvmulxxbr  15493  dvcoapbr  15498  dvrecap  15504  pellexlem3  15773  sgmval2  15778  sgmmul  15790  perfectlem2  15794  lgsfcl  15807  lgscl  15813  lgsquadlem1  15876  lgsquadlem2  15877  incistruhgr  16011  upgrss  16020  usgrss  16098  ushgredgedg  16147  ushgredgedgloop  16149  vtxdfifiun  16218  bdrabexg  16602  2omap  16695  pw1map  16697  subctctexmid  16702