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  4228  pwnss  4244  undifexmid  4278  exmidexmid  4281  exmidsssnc  4288  onintrab2im  4611  ordtriexmidlem  4612  ontr2exmid  4618  ordtri2or2exmidlem  4619  onsucsssucexmid  4620  onsucelsucexmidlem  4622  tfis  4676  nnregexmid  4714  dmmptss  5228  ssimaex  5700  f1oresrab  5805  canth  5961  riotacl  5979  pmvalg  6819  ssfiexmid  7051  domfiexmid  7053  ctssdccl  7294  ctssexmid  7333  genpelxp  7714  ltexprlempr  7811  cauappcvgprlemcl  7856  cauappcvgprlemladd  7861  caucvgprlemcl  7879  caucvgprprlemcl  7907  suplocexprlemex  7925  uzf  9741  supminfex  9809  rpre  9873  ixxf  10111  fzf  10225  infssuzex  10470  infssuzcldc  10472  zsupssdc  10475  expcl2lemap  10790  expclzaplem  10802  expge0  10814  expge1  10815  dvdsflip  12383  bitsf  12478  bitsfzolem  12486  gcddvds  12505  uzwodc  12579  nnwosdc  12581  nninfctlemfo  12582  lcmn0cl  12611  phicl2  12757  phimullem  12768  eulerthlemfi  12771  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemh  12774  eulerthlemth  12775  phisum  12784  pcpremul  12837  ennnfonelemg  12995  ennnfonelemh  12996  ctiunctlemuom  13028  issubmd  13528  mhmeql  13546  lspf  14374  mplbascoe  14676  mplbasss  14681  epttop  14785  neipsm  14849  cnpfval  14890  blfvalps  15080  blfps  15104  blf  15105  divcnap  15260  cdivcncfap  15299  cnopnap  15306  ivthinclemex  15337  limcdifap  15357  dvfgg  15383  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvrecap  15408  sgmval2  15679  sgmmul  15691  perfectlem2  15695  lgsfcl  15708  lgscl  15714  lgsquadlem1  15777  lgsquadlem2  15778  incistruhgr  15911  upgrss  15920  usgrss  15996  ushgredgedg  16045  ushgredgedgloop  16047  vtxdfifiun  16083  bdrabexg  16378  2omap  16472  pw1map  16474  subctctexmid  16479