Theorem ssrab2 3280

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

Syntax hints:   ∧ wa 104   ∈ wcel 2177  {cab 2192  {crab 2489   ⊆ wss 3168

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-in 3174  df-ss 3181

This theorem is referenced by:  ssrab3  3281  ssrabeq  3282  ifssun  3587  rabexg  4192  pwnss  4208  undifexmid  4242  exmidexmid  4245  exmidsssnc  4252  onintrab2im  4571  ordtriexmidlem  4572  ontr2exmid  4578  ordtri2or2exmidlem  4579  onsucsssucexmid  4580  onsucelsucexmidlem  4582  tfis  4636  nnregexmid  4674  dmmptss  5185  ssimaex  5650  f1oresrab  5755  canth  5907  riotacl  5924  pmvalg  6756  ssfiexmid  6985  domfiexmid  6987  ctssdccl  7225  ctssexmid  7264  genpelxp  7637  ltexprlempr  7734  cauappcvgprlemcl  7779  cauappcvgprlemladd  7784  caucvgprlemcl  7802  caucvgprprlemcl  7830  suplocexprlemex  7848  uzf  9664  supminfex  9731  rpre  9795  ixxf  10033  fzf  10147  infssuzex  10389  infssuzcldc  10391  zsupssdc  10394  expcl2lemap  10709  expclzaplem  10721  expge0  10733  expge1  10734  dvdsflip  12212  bitsf  12307  bitsfzolem  12315  gcddvds  12334  uzwodc  12408  nnwosdc  12410  nninfctlemfo  12411  lcmn0cl  12440  phicl2  12586  phimullem  12597  eulerthlemfi  12600  eulerthlemrprm  12601  eulerthlema  12602  eulerthlemh  12603  eulerthlemth  12604  phisum  12613  pcpremul  12666  ennnfonelemg  12824  ennnfonelemh  12825  ctiunctlemuom  12857  issubmd  13356  mhmeql  13374  lspf  14201  mplbascoe  14503  mplbasss  14508  epttop  14612  neipsm  14676  cnpfval  14717  blfvalps  14907  blfps  14931  blf  14932  divcnap  15087  cdivcncfap  15126  cnopnap  15133  ivthinclemex  15164  limcdifap  15184  dvfgg  15210  dvidlemap  15213  dvidrelem  15214  dvidsslem  15215  dvcnp2cntop  15221  dvaddxxbr  15223  dvmulxxbr  15224  dvcoapbr  15229  dvrecap  15235  sgmval2  15506  sgmmul  15518  perfectlem2  15522  lgsfcl  15535  lgscl  15541  lgsquadlem1  15604  lgsquadlem2  15605  incistruhgr  15736  upgrss  15745  bdrabexg  15956  2omap  16047  subctctexmid  16052