Theorem ssrab2 3310

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 3309	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
3	1, 2	eqsstri 3257	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   ∧ wa 104   ∈ wcel 2200  {cab 2215  {crab 2512   ⊆ wss 3198

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 3204  df-ss 3211

This theorem is referenced by:  ssrab3  3311  ssrabeq  3312  ifssun  3618  rabexg  4229  pwnss  4245  undifexmid  4279  exmidexmid  4282  exmidsssnc  4289  onintrab2im  4612  ordtriexmidlem  4613  ontr2exmid  4619  ordtri2or2exmidlem  4620  onsucsssucexmid  4621  onsucelsucexmidlem  4623  tfis  4677  nnregexmid  4715  dmmptss  5229  ssimaex  5701  f1oresrab  5806  canth  5962  riotacl  5980  pmvalg  6821  ssfiexmid  7056  domfiexmid  7058  ctssdccl  7299  ctssexmid  7338  genpelxp  7719  ltexprlempr  7816  cauappcvgprlemcl  7861  cauappcvgprlemladd  7866  caucvgprlemcl  7884  caucvgprprlemcl  7912  suplocexprlemex  7930  uzf  9746  supminfex  9819  rpre  9883  ixxf  10121  fzf  10235  infssuzex  10481  infssuzcldc  10483  zsupssdc  10486  expcl2lemap  10801  expclzaplem  10813  expge0  10825  expge1  10826  dvdsflip  12399  bitsf  12494  bitsfzolem  12502  gcddvds  12521  uzwodc  12595  nnwosdc  12597  nninfctlemfo  12598  lcmn0cl  12627  phicl2  12773  phimullem  12784  eulerthlemfi  12787  eulerthlemrprm  12788  eulerthlema  12789  eulerthlemh  12790  eulerthlemth  12791  phisum  12800  pcpremul  12853  ennnfonelemg  13011  ennnfonelemh  13012  ctiunctlemuom  13044  issubmd  13544  mhmeql  13562  lspf  14390  mplbascoe  14692  mplbasss  14697  epttop  14801  neipsm  14865  cnpfval  14906  blfvalps  15096  blfps  15120  blf  15121  divcnap  15276  cdivcncfap  15315  cnopnap  15322  ivthinclemex  15353  limcdifap  15373  dvfgg  15399  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404  dvcnp2cntop  15410  dvaddxxbr  15412  dvmulxxbr  15413  dvcoapbr  15418  dvrecap  15424  sgmval2  15695  sgmmul  15707  perfectlem2  15711  lgsfcl  15724  lgscl  15730  lgsquadlem1  15793  lgsquadlem2  15794  incistruhgr  15927  upgrss  15936  usgrss  16012  ushgredgedg  16061  ushgredgedgloop  16063  vtxdfifiun  16099  bdrabexg  16411  2omap  16504  pw1map  16506  subctctexmid  16511