Theorem ssrab2 3327

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

Syntax hints:   ∧ wa 104   ∈ wcel 2205  {cab 2220  {crab 2526   ⊆ wss 3214

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3220  df-ss 3227

This theorem is referenced by:  ssrab3  3328  ssrabeq  3330  ifssun  3641  rabexg  4260  pwnss  4277  undifexmid  4311  exmidexmid  4314  exmidsssnc  4321  onintrab2im  4645  ordtriexmidlem  4646  ontr2exmid  4652  ordtri2or2exmidlem  4653  onsucsssucexmid  4654  onsucelsucexmidlem  4656  tfis  4710  nnregexmid  4748  dmmptss  5264  ssimaex  5743  f1oresrab  5847  canth  6009  riotacl  6027  suppssdmg  6462  pmvalg  6906  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  2omap  7282  ctssdccl  7415  ctssexmid  7454  genpelxp  7842  ltexprlempr  7939  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  suplocexprlemex  8053  uzf  9877  supminfex  9950  rpre  10014  ixxf  10253  fzf  10368  infssuzex  10618  infssuzcldc  10620  zsupssdc  10625  expcl2lemap  10940  expclzaplem  10952  expge0  10964  expge1  10965  dvdsflip  12566  bitsf  12661  bitsfzolem  12669  gcddvds  12688  uzwodc  12762  nnwosdc  12764  nninfctlemfo  12765  lcmn0cl  12794  phicl2  12940  phimullem  12951  eulerthlemfi  12954  eulerthlemrprm  12955  eulerthlema  12956  eulerthlemh  12957  eulerthlemth  12958  phisum  12967  pcpremul  13020  ballotfilem2  13176  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemiex  13192  ballotfilem7  13227  ballotfilemth  13229  ennnfonelemg  13242  ennnfonelemh  13243  ctiunctlemuom  13275  issubmd  13733  mhmeql  13751  lspf  14667  mplbascoe  14976  mplbasss  14981  epttop  15085  neipsm  15149  cnpfval  15190  blfvalps  15380  blfps  15404  blf  15405  divcnap  15560  cdivcncfap  15599  cnopnap  15606  ivthinclemex  15637  limcdifap  15657  dvfgg  15683  dvidlemap  15686  dvidrelem  15687  dvidsslem  15688  dvcnp2cntop  15694  dvaddxxbr  15696  dvmulxxbr  15697  dvcoapbr  15702  dvrecap  15708  pellexlem3  15977  sgmval2  15982  sgmmul  15994  perfectlem2  15998  lgsfcl  16011  lgscl  16017  lgsquadlem1  16080  lgsquadlem2  16081  incistruhgr  16215  upgrss  16224  usgrss  16302  ushgredgedg  16351  ushgredgedgloop  16353  vtxdfifiun  16422  bdrabexg  16816  pw1map  16909  subctctexmid  16914