Theorem ssrab2 3333

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

This proof depends on syntax axioms:   ∧ wa 104   ∈ wcel 2209  {cab 2224  {crab 2532   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233

This theorem is used by:  ssrab3  3334  ssrabeq  3336  ifssun  3655  rabexg  4281  pwnss  4298  undifexmid  4332  exmidexmid  4335  exmidsssnc  4342  onintrab2im  4667  ordtriexmidlem  4668  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucsssucexmid  4676  onsucelsucexmidlem  4678  tfis  4732  nnregexmid  4770  dmmptss  5287  ssimaex  5767  f1oresrab  5876  canth  6039  riotacl  6057  suppssdmg  6493  pmvalg  6937  ssfiexmid  7183  ssfiexmidt  7185  domfiexmid  7187  2omap  7325  ctssdccl  7458  ctssexmid  7497  genpelxp  7885  ltexprlempr  7982  cauappcvgprlemcl  8027  cauappcvgprlemladd  8032  caucvgprlemcl  8050  caucvgprprlemcl  8078  suplocexprlemex  8096  uzf  9941  supminfex  10014  rpre  10079  ixxf  10318  fzf  10433  infssuzex  10684  infssuzcldc  10686  zsupssdc  10691  expcl2lemap  11010  expclzaplem  11022  expge0  11034  expge1  11035  dvdsflip  12644  bitsf  12739  bitsfzolem  12747  gcddvds  12766  uzwodc  12840  nnwosdc  12842  nninfctlemfo  12843  lcmn0cl  12872  phicl2  13022  phimullem  13033  eulerthlemfi  13036  eulerthlemrprm  13037  eulerthlema  13038  eulerthlemh  13039  eulerthlemth  13040  phisum  13049  pcpremul  13102  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemiex  13303  ballotfilem7  13338  ballotfilemth  13340  ennnfonelemg  13353  ennnfonelemh  13354  ctiunctlemuom  13386  issubmd  13841  mhmeql  13859  cntzssv  14161  lspf  14836  asplss  15126  aspsubrg  15128  psrass1filem  15182  psrdifi  15207  psrdirfi  15208  mplbascoe  15219  mplbasss  15224  epttop  15328  neipsm  15392  cnpfval  15433  blfvalps  15623  blfps  15647  blf  15648  divcnap  15803  cdivcncfap  15842  cnopnap  15849  ivthinclemex  15880  limcdifap  15900  dvfgg  15926  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvcnp2cntop  15937  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvrecap  15951  pellexlem3  16243  efnnfsumcl  16251  sgmval2  16265  efchtqdvds  16277  sgmmul  16302  ppiqub  16305  perfectlem2  16312  lgsfcl  16344  lgscl  16350  lgsquadlem1  16413  lgsquadlem2  16414  incistruhgr  16548  upgrss  16557  usgrss  16635  ushgredgedg  16684  ushgredgedgloop  16686  vtxdfifiun  16755  bdrabexg  17149  pw1map  17242  subctctexmid  17247  stnot  17256  wexmiddc  17259