Theorem ssrab2 3309

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

Syntax hints:   ∧ wa 104   ∈ wcel 2200  {cab 2215  {crab 2512   ⊆ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210

This theorem is referenced by:  ssrab3  3310  ssrabeq  3311  ifssun  3617  rabexg  4227  pwnss  4243  undifexmid  4277  exmidexmid  4280  exmidsssnc  4287  onintrab2im  4610  ordtriexmidlem  4611  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  onsucelsucexmidlem  4621  tfis  4675  nnregexmid  4713  dmmptss  5225  ssimaex  5697  f1oresrab  5802  canth  5958  riotacl  5976  pmvalg  6814  ssfiexmid  7046  domfiexmid  7048  ctssdccl  7286  ctssexmid  7325  genpelxp  7706  ltexprlempr  7803  cauappcvgprlemcl  7848  cauappcvgprlemladd  7853  caucvgprlemcl  7871  caucvgprprlemcl  7899  suplocexprlemex  7917  uzf  9733  supminfex  9800  rpre  9864  ixxf  10102  fzf  10216  infssuzex  10461  infssuzcldc  10463  zsupssdc  10466  expcl2lemap  10781  expclzaplem  10793  expge0  10805  expge1  10806  dvdsflip  12370  bitsf  12465  bitsfzolem  12473  gcddvds  12492  uzwodc  12566  nnwosdc  12568  nninfctlemfo  12569  lcmn0cl  12598  phicl2  12744  phimullem  12755  eulerthlemfi  12758  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemh  12761  eulerthlemth  12762  phisum  12771  pcpremul  12824  ennnfonelemg  12982  ennnfonelemh  12983  ctiunctlemuom  13015  issubmd  13515  mhmeql  13533  lspf  14361  mplbascoe  14663  mplbasss  14668  epttop  14772  neipsm  14836  cnpfval  14877  blfvalps  15067  blfps  15091  blf  15092  divcnap  15247  cdivcncfap  15286  cnopnap  15293  ivthinclemex  15324  limcdifap  15344  dvfgg  15370  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvcnp2cntop  15381  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvrecap  15395  sgmval2  15666  sgmmul  15678  perfectlem2  15682  lgsfcl  15695  lgscl  15701  lgsquadlem1  15764  lgsquadlem2  15765  incistruhgr  15898  upgrss  15907  usgrss  15983  ushgredgedg  16032  ushgredgedgloop  16034  bdrabexg  16293  2omap  16388  pw1map  16390  subctctexmid  16395