Theorem ssrab2 3241

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

Syntax hints:   ∧ wa 104   ∈ wcel 2148  {cab 2163  {crab 2459   ⊆ wss 3130

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3136  df-ss 3143

This theorem is referenced by:  ssrab3  3242  ssrabeq  3243  ifssun  3549  rabexg  4147  pwnss  4160  undifexmid  4194  exmidexmid  4197  exmidsssnc  4204  onintrab2im  4518  ordtriexmidlem  4519  ontr2exmid  4525  ordtri2or2exmidlem  4526  onsucsssucexmid  4527  onsucelsucexmidlem  4529  tfis  4583  nnregexmid  4621  dmmptss  5126  ssimaex  5578  f1oresrab  5682  canth  5829  riotacl  5845  pmvalg  6659  ssfiexmid  6876  domfiexmid  6878  ctssdccl  7110  ctssexmid  7148  genpelxp  7510  ltexprlempr  7607  cauappcvgprlemcl  7652  cauappcvgprlemladd  7657  caucvgprlemcl  7675  caucvgprprlemcl  7703  suplocexprlemex  7721  uzf  9531  supminfex  9597  rpre  9660  ixxf  9898  fzf  10012  expcl2lemap  10532  expclzaplem  10544  expge0  10556  expge1  10557  dvdsflip  11857  infssuzex  11950  infssuzcldc  11952  zsupssdc  11955  gcddvds  11964  uzwodc  12038  nnwosdc  12040  lcmn0cl  12068  phicl2  12214  phimullem  12225  eulerthlemfi  12228  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  phisum  12240  pcpremul  12293  ennnfonelemg  12404  ennnfonelemh  12405  ctiunctlemuom  12437  issubmd  12865  mhmeql  12876  epttop  13593  neipsm  13657  cnpfval  13698  blfvalps  13888  blfps  13912  blf  13913  divcnap  14058  cdivcncfap  14090  cnopnap  14097  ivthinclemex  14123  limcdifap  14134  dvfgg  14160  dvidlemap  14163  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvrecap  14180  lgsfcl  14412  lgscl  14418  bdrabexg  14661  subctctexmid  14753