Theorem ssrab2 3088

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

Syntax hints:   ∧ wa 102   ∈ wcel 1434  {cab 2069  {crab 2357   ⊆ wss 2982

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rab 2362  df-in 2988  df-ss 2995

This theorem is referenced by:  ssrabeq  3089  rabexg  3941  pwnss  3953  undifexmid  3984  exmidexmid  3987  onintrab2im  4290  ordtriexmidlem  4291  ontr2exmid  4296  ordtri2or2exmidlem  4297  onsucsssucexmid  4298  onsucelsucexmidlem  4300  tfis  4352  nnregexmid  4388  dmmptss  4867  ssimaex  5286  f1oresrab  5381  riotacl  5533  ssfiexmid  6432  domfiexmid  6434  genpelxp  6815  ltexprlempr  6912  cauappcvgprlemcl  6957  cauappcvgprlemladd  6962  caucvgprlemcl  6980  caucvgprprlemcl  7008  uzf  8755  supminfex  8818  rpre  8873  ixxf  9049  fzf  9161  serige0  9622  expcl2lemap  9637  expclzaplem  9649  expge0  9661  expge1  9662  dvdsflip  10459  infssuzex  10552  infssuzcldc  10554  gcddvds  10562  lcmn0cl  10657  phicl2  10797  phimullem  10808  bdrabexg  10964