Theorem ssrab2 3187

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

Syntax hints:   ∧ wa 103   ∈ wcel 1481  {cab 2126  {crab 2421   ⊆ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-in 3082  df-ss 3089

This theorem is referenced by:  ssrabeq  3188  rabexg  4079  pwnss  4091  undifexmid  4125  exmidexmid  4128  exmidsssnc  4134  onintrab2im  4442  ordtriexmidlem  4443  ontr2exmid  4448  ordtri2or2exmidlem  4449  onsucsssucexmid  4450  onsucelsucexmidlem  4452  tfis  4505  nnregexmid  4542  dmmptss  5043  ssimaex  5490  f1oresrab  5593  riotacl  5752  pmvalg  6561  ssfiexmid  6778  domfiexmid  6780  ctssdccl  7004  ctssexmid  7032  genpelxp  7343  ltexprlempr  7440  cauappcvgprlemcl  7485  cauappcvgprlemladd  7490  caucvgprlemcl  7508  caucvgprprlemcl  7536  suplocexprlemex  7554  uzf  9353  supminfex  9419  rpre  9477  ixxf  9711  fzf  9825  expcl2lemap  10336  expclzaplem  10348  expge0  10360  expge1  10361  dvdsflip  11585  infssuzex  11678  infssuzcldc  11680  gcddvds  11688  lcmn0cl  11785  phicl2  11926  phimullem  11937  ennnfonelemg  11952  ennnfonelemh  11953  ctiunctlemuom  11985  epttop  12298  neipsm  12362  cnpfval  12403  blfvalps  12593  blfps  12617  blf  12618  divcnap  12763  cdivcncfap  12795  cnopnap  12802  ivthinclemex  12828  limcdifap  12839  dvfgg  12865  dvidlemap  12868  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvrecap  12885  bdrabexg  13275  subctctexmid  13369