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  9874  supminfex  9947  rpre  10011  ixxf  10250  fzf  10365  infssuzex  10615  infssuzcldc  10617  zsupssdc  10622  expcl2lemap  10937  expclzaplem  10949  expge0  10961  expge1  10962  dvdsflip  12562  bitsf  12657  bitsfzolem  12665  gcddvds  12684  uzwodc  12758  nnwosdc  12760  nninfctlemfo  12761  lcmn0cl  12790  phicl2  12936  phimullem  12947  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  phisum  12963  pcpremul  13016  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemiex  13188  ballotfilem7  13223  ballotfilemth  13225  ennnfonelemg  13238  ennnfonelemh  13239  ctiunctlemuom  13271  issubmd  13771  mhmeql  13789  lspf  14649  mplbascoe  14958  mplbasss  14963  epttop  15067  neipsm  15131  cnpfval  15172  blfvalps  15362  blfps  15386  blf  15387  divcnap  15542  cdivcncfap  15581  cnopnap  15588  ivthinclemex  15619  limcdifap  15639  dvfgg  15665  dvidlemap  15668  dvidrelem  15669  dvidsslem  15670  dvcnp2cntop  15676  dvaddxxbr  15678  dvmulxxbr  15679  dvcoapbr  15684  dvrecap  15690  pellexlem3  15959  sgmval2  15964  sgmmul  15976  perfectlem2  15980  lgsfcl  15993  lgscl  15999  lgsquadlem1  16062  lgsquadlem2  16063  incistruhgr  16197  upgrss  16206  usgrss  16284  ushgredgedg  16333  ushgredgedgloop  16335  vtxdfifiun  16404  bdrabexg  16788  pw1map  16881  subctctexmid  16886