Theorem ssrab2 3213

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

Syntax hints:   ∧ wa 103   ∈ wcel 2128  {cab 2143  {crab 2439   ⊆ wss 3102

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-in 3108  df-ss 3115

This theorem is referenced by:  ssrabeq  3214  ifssun  3519  rabexg  4107  pwnss  4120  undifexmid  4154  exmidexmid  4157  exmidsssnc  4164  onintrab2im  4476  ordtriexmidlem  4477  ontr2exmid  4483  ordtri2or2exmidlem  4484  onsucsssucexmid  4485  onsucelsucexmidlem  4487  tfis  4541  nnregexmid  4579  dmmptss  5081  ssimaex  5528  f1oresrab  5631  canth  5775  riotacl  5791  pmvalg  6601  ssfiexmid  6818  domfiexmid  6820  ctssdccl  7050  ctssexmid  7088  genpelxp  7426  ltexprlempr  7523  cauappcvgprlemcl  7568  cauappcvgprlemladd  7573  caucvgprlemcl  7591  caucvgprprlemcl  7619  suplocexprlemex  7637  uzf  9437  supminfex  9503  rpre  9562  ixxf  9797  fzf  9911  expcl2lemap  10426  expclzaplem  10438  expge0  10450  expge1  10451  dvdsflip  11737  infssuzex  11830  infssuzcldc  11832  gcddvds  11841  lcmn0cl  11939  phicl2  12081  phimullem  12092  eulerthlemfi  12095  eulerthlemrprm  12096  eulerthlema  12097  eulerthlemh  12098  eulerthlemth  12099  phisum  12107  ennnfonelemg  12119  ennnfonelemh  12120  ctiunctlemuom  12152  epttop  12477  neipsm  12541  cnpfval  12582  blfvalps  12772  blfps  12796  blf  12797  divcnap  12942  cdivcncfap  12974  cnopnap  12981  ivthinclemex  13007  limcdifap  13018  dvfgg  13044  dvidlemap  13047  dvcnp2cntop  13050  dvaddxxbr  13052  dvmulxxbr  13053  dvcoapbr  13058  dvrecap  13064  bdrabexg  13468  subctctexmid  13560