Theorem ssrab2 3252

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

Syntax hints:   ∧ wa 104   ∈ wcel 2158  {cab 2173  {crab 2469   ⊆ wss 3141

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rab 2474  df-in 3147  df-ss 3154

This theorem is referenced by:  ssrab3  3253  ssrabeq  3254  ifssun  3560  rabexg  4158  pwnss  4171  undifexmid  4205  exmidexmid  4208  exmidsssnc  4215  onintrab2im  4529  ordtriexmidlem  4530  ontr2exmid  4536  ordtri2or2exmidlem  4537  onsucsssucexmid  4538  onsucelsucexmidlem  4540  tfis  4594  nnregexmid  4632  dmmptss  5137  ssimaex  5590  f1oresrab  5694  canth  5842  riotacl  5858  pmvalg  6673  ssfiexmid  6890  domfiexmid  6892  ctssdccl  7124  ctssexmid  7162  genpelxp  7524  ltexprlempr  7621  cauappcvgprlemcl  7666  cauappcvgprlemladd  7671  caucvgprlemcl  7689  caucvgprprlemcl  7717  suplocexprlemex  7735  uzf  9545  supminfex  9611  rpre  9674  ixxf  9912  fzf  10026  expcl2lemap  10546  expclzaplem  10558  expge0  10570  expge1  10571  dvdsflip  11871  infssuzex  11964  infssuzcldc  11966  zsupssdc  11969  gcddvds  11978  uzwodc  12052  nnwosdc  12054  lcmn0cl  12082  phicl2  12228  phimullem  12239  eulerthlemfi  12242  eulerthlemrprm  12243  eulerthlema  12244  eulerthlemh  12245  eulerthlemth  12246  phisum  12254  pcpremul  12307  ennnfonelemg  12418  ennnfonelemh  12419  ctiunctlemuom  12451  issubmd  12887  mhmeql  12898  lspf  13578  epttop  13886  neipsm  13950  cnpfval  13991  blfvalps  14181  blfps  14205  blf  14206  divcnap  14351  cdivcncfap  14383  cnopnap  14390  ivthinclemex  14416  limcdifap  14427  dvfgg  14453  dvidlemap  14456  dvcnp2cntop  14459  dvaddxxbr  14461  dvmulxxbr  14462  dvcoapbr  14467  dvrecap  14473  lgsfcl  14705  lgscl  14711  bdrabexg  14954  subctctexmid  15047