Theorem ssrab2 3310

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 3309	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
3	1, 2	eqsstri 3257	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

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

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 3204  df-ss 3211

This theorem is referenced by:  ssrab3  3311  ssrabeq  3312  ifssun  3618  rabexg  4231  pwnss  4247  undifexmid  4281  exmidexmid  4284  exmidsssnc  4291  onintrab2im  4614  ordtriexmidlem  4615  ontr2exmid  4621  ordtri2or2exmidlem  4622  onsucsssucexmid  4623  onsucelsucexmidlem  4625  tfis  4679  nnregexmid  4717  dmmptss  5231  ssimaex  5703  f1oresrab  5808  canth  5964  riotacl  5982  pmvalg  6823  ssfiexmid  7058  ssfiexmidt  7060  domfiexmid  7062  ctssdccl  7304  ctssexmid  7343  genpelxp  7724  ltexprlempr  7821  cauappcvgprlemcl  7866  cauappcvgprlemladd  7871  caucvgprlemcl  7889  caucvgprprlemcl  7917  suplocexprlemex  7935  uzf  9751  supminfex  9824  rpre  9888  ixxf  10126  fzf  10240  infssuzex  10486  infssuzcldc  10488  zsupssdc  10491  expcl2lemap  10806  expclzaplem  10818  expge0  10830  expge1  10831  dvdsflip  12405  bitsf  12500  bitsfzolem  12508  gcddvds  12527  uzwodc  12601  nnwosdc  12603  nninfctlemfo  12604  lcmn0cl  12633  phicl2  12779  phimullem  12790  eulerthlemfi  12793  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemh  12796  eulerthlemth  12797  phisum  12806  pcpremul  12859  ennnfonelemg  13017  ennnfonelemh  13018  ctiunctlemuom  13050  issubmd  13550  mhmeql  13568  lspf  14396  mplbascoe  14698  mplbasss  14703  epttop  14807  neipsm  14871  cnpfval  14912  blfvalps  15102  blfps  15126  blf  15127  divcnap  15282  cdivcncfap  15321  cnopnap  15328  ivthinclemex  15359  limcdifap  15379  dvfgg  15405  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvcnp2cntop  15416  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvrecap  15430  sgmval2  15701  sgmmul  15713  perfectlem2  15717  lgsfcl  15730  lgscl  15736  lgsquadlem1  15799  lgsquadlem2  15800  incistruhgr  15934  upgrss  15943  usgrss  16021  ushgredgedg  16070  ushgredgedgloop  16072  vtxdfifiun  16108  bdrabexg  16451  2omap  16544  pw1map  16546  subctctexmid  16551