Theorem ssrab2 3226

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

Syntax hints:   ∧ wa 103   ∈ wcel 2136  {cab 2151  {crab 2447   ⊆ wss 3115

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rab 2452  df-in 3121  df-ss 3128

This theorem is referenced by:  ssrab3  3227  ssrabeq  3228  ifssun  3533  rabexg  4124  pwnss  4137  undifexmid  4171  exmidexmid  4174  exmidsssnc  4181  onintrab2im  4494  ordtriexmidlem  4495  ontr2exmid  4501  ordtri2or2exmidlem  4502  onsucsssucexmid  4503  onsucelsucexmidlem  4505  tfis  4559  nnregexmid  4597  dmmptss  5099  ssimaex  5546  f1oresrab  5649  canth  5795  riotacl  5811  pmvalg  6621  ssfiexmid  6838  domfiexmid  6840  ctssdccl  7072  ctssexmid  7110  genpelxp  7448  ltexprlempr  7545  cauappcvgprlemcl  7590  cauappcvgprlemladd  7595  caucvgprlemcl  7613  caucvgprprlemcl  7641  suplocexprlemex  7659  uzf  9465  supminfex  9531  rpre  9592  ixxf  9830  fzf  9944  expcl2lemap  10463  expclzaplem  10475  expge0  10487  expge1  10488  dvdsflip  11785  infssuzex  11878  infssuzcldc  11880  zsupssdc  11883  gcddvds  11892  uzwodc  11966  nnwosdc  11968  lcmn0cl  11996  phicl2  12142  phimullem  12153  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  phisum  12168  pcpremul  12221  ennnfonelemg  12332  ennnfonelemh  12333  ctiunctlemuom  12365  epttop  12690  neipsm  12754  cnpfval  12795  blfvalps  12985  blfps  13009  blf  13010  divcnap  13155  cdivcncfap  13187  cnopnap  13194  ivthinclemex  13220  limcdifap  13231  dvfgg  13257  dvidlemap  13260  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvrecap  13277  lgsfcl  13509  lgscl  13515  bdrabexg  13748  subctctexmid  13841