Theorem ssrab2 3232

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

Syntax hints:   ∧ wa 103   ∈ wcel 2141  {cab 2156  {crab 2452   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rab 2457  df-in 3127  df-ss 3134

This theorem is referenced by:  ssrab3  3233  ssrabeq  3234  ifssun  3540  rabexg  4132  pwnss  4145  undifexmid  4179  exmidexmid  4182  exmidsssnc  4189  onintrab2im  4502  ordtriexmidlem  4503  ontr2exmid  4509  ordtri2or2exmidlem  4510  onsucsssucexmid  4511  onsucelsucexmidlem  4513  tfis  4567  nnregexmid  4605  dmmptss  5107  ssimaex  5557  f1oresrab  5661  canth  5807  riotacl  5823  pmvalg  6637  ssfiexmid  6854  domfiexmid  6856  ctssdccl  7088  ctssexmid  7126  genpelxp  7473  ltexprlempr  7570  cauappcvgprlemcl  7615  cauappcvgprlemladd  7620  caucvgprlemcl  7638  caucvgprprlemcl  7666  suplocexprlemex  7684  uzf  9490  supminfex  9556  rpre  9617  ixxf  9855  fzf  9969  expcl2lemap  10488  expclzaplem  10500  expge0  10512  expge1  10513  dvdsflip  11811  infssuzex  11904  infssuzcldc  11906  zsupssdc  11909  gcddvds  11918  uzwodc  11992  nnwosdc  11994  lcmn0cl  12022  phicl2  12168  phimullem  12179  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  phisum  12194  pcpremul  12247  ennnfonelemg  12358  ennnfonelemh  12359  ctiunctlemuom  12391  issubmd  12696  mhmeql  12707  epttop  12884  neipsm  12948  cnpfval  12989  blfvalps  13179  blfps  13203  blf  13204  divcnap  13349  cdivcncfap  13381  cnopnap  13388  ivthinclemex  13414  limcdifap  13425  dvfgg  13451  dvidlemap  13454  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvrecap  13471  lgsfcl  13703  lgscl  13709  bdrabexg  13941  subctctexmid  14034