Theorem ssrab2 3312

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

Syntax hints:   ∧ wa 104   ∈ wcel 2202  {cab 2217  {crab 2514   ⊆ wss 3200

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213

This theorem is referenced by:  ssrab3  3313  ssrabeq  3314  ifssun  3620  rabexg  4233  pwnss  4249  undifexmid  4283  exmidexmid  4286  exmidsssnc  4293  onintrab2im  4616  ordtriexmidlem  4617  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucsssucexmid  4625  onsucelsucexmidlem  4627  tfis  4681  nnregexmid  4719  dmmptss  5233  ssimaex  5707  f1oresrab  5812  canth  5969  riotacl  5987  pmvalg  6828  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  ctssdccl  7310  ctssexmid  7349  genpelxp  7731  ltexprlempr  7828  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocexprlemex  7942  uzf  9758  supminfex  9831  rpre  9895  ixxf  10133  fzf  10247  infssuzex  10494  infssuzcldc  10496  zsupssdc  10499  expcl2lemap  10814  expclzaplem  10826  expge0  10838  expge1  10839  dvdsflip  12417  bitsf  12512  bitsfzolem  12520  gcddvds  12539  uzwodc  12613  nnwosdc  12615  nninfctlemfo  12616  lcmn0cl  12645  phicl2  12791  phimullem  12802  eulerthlemfi  12805  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  phisum  12818  pcpremul  12871  ennnfonelemg  13029  ennnfonelemh  13030  ctiunctlemuom  13062  issubmd  13562  mhmeql  13580  lspf  14409  mplbascoe  14711  mplbasss  14716  epttop  14820  neipsm  14884  cnpfval  14925  blfvalps  15115  blfps  15139  blf  15140  divcnap  15295  cdivcncfap  15334  cnopnap  15341  ivthinclemex  15372  limcdifap  15392  dvfgg  15418  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvcnp2cntop  15429  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  dvrecap  15443  sgmval2  15714  sgmmul  15726  perfectlem2  15730  lgsfcl  15743  lgscl  15749  lgsquadlem1  15812  lgsquadlem2  15813  incistruhgr  15947  upgrss  15956  usgrss  16034  ushgredgedg  16083  ushgredgedgloop  16085  vtxdfifiun  16154  bdrabexg  16527  2omap  16620  pw1map  16622  subctctexmid  16627