Theorem ssrab2 3322

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

Syntax hints:   ∧ wa 104   ∈ wcel 2203  {cab 2218  {crab 2524   ⊆ wss 3210

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rab 2529  df-in 3216  df-ss 3223

This theorem is referenced by:  ssrab3  3323  ssrabeq  3325  ifssun  3636  rabexg  4254  pwnss  4271  undifexmid  4305  exmidexmid  4308  exmidsssnc  4315  onintrab2im  4639  ordtriexmidlem  4640  ontr2exmid  4646  ordtri2or2exmidlem  4647  onsucsssucexmid  4648  onsucelsucexmidlem  4650  tfis  4704  nnregexmid  4742  dmmptss  5258  ssimaex  5737  f1oresrab  5841  canth  6000  riotacl  6018  suppssdmg  6448  pmvalg  6892  ssfiexmid  7130  ssfiexmidt  7132  domfiexmid  7134  2omap  7268  ctssdccl  7401  ctssexmid  7440  genpelxp  7825  ltexprlempr  7922  cauappcvgprlemcl  7967  cauappcvgprlemladd  7972  caucvgprlemcl  7990  caucvgprprlemcl  8018  suplocexprlemex  8036  uzf  9855  supminfex  9928  rpre  9992  ixxf  10230  fzf  10345  infssuzex  10592  infssuzcldc  10594  zsupssdc  10597  expcl2lemap  10912  expclzaplem  10924  expge0  10936  expge1  10937  dvdsflip  12533  bitsf  12628  bitsfzolem  12636  gcddvds  12655  uzwodc  12729  nnwosdc  12731  nninfctlemfo  12732  lcmn0cl  12761  phicl2  12907  phimullem  12918  eulerthlemfi  12921  eulerthlemrprm  12922  eulerthlema  12923  eulerthlemh  12924  eulerthlemth  12925  phisum  12934  pcpremul  12987  ennnfonelemg  13146  ennnfonelemh  13147  ctiunctlemuom  13179  issubmd  13679  mhmeql  13697  lspf  14529  mplbascoe  14838  mplbasss  14843  epttop  14947  neipsm  15011  cnpfval  15052  blfvalps  15242  blfps  15266  blf  15267  divcnap  15422  cdivcncfap  15461  cnopnap  15468  ivthinclemex  15499  limcdifap  15519  dvfgg  15545  dvidlemap  15548  dvidrelem  15549  dvidsslem  15550  dvcnp2cntop  15556  dvaddxxbr  15558  dvmulxxbr  15559  dvcoapbr  15564  dvrecap  15570  pellexlem3  15839  sgmval2  15844  sgmmul  15856  perfectlem2  15860  lgsfcl  15873  lgscl  15879  lgsquadlem1  15942  lgsquadlem2  15943  incistruhgr  16077  upgrss  16086  usgrss  16164  ushgredgedg  16213  ushgredgedgloop  16215  vtxdfifiun  16284  bdrabexg  16668  pw1map  16761  subctctexmid  16766