Theorem ss2abi 4028

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2151, ax-10 2182, ax-11 2198, ax-12 2219. (Revised by GG, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ss2abi	⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Proof of Theorem ss2abi

Step	Hyp	Ref	Expression
1		ss2abi.1	. . . 4 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
3	2	ss2abdv 4027	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1574	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1568  {cab 2747   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-sb 2098  df-clab 2748  df-ss 3930

This theorem is referenced by:  abssi  4030  rabssab  4047  abanssl  4272  abanssr  4273  pwpwssunieq  5074  intabs  5320  abssexg  5354  imassrn  6074  fvclss  7240  mapex  7937  f1osetex  8856  fsetexb  8861  tc2  9709  hta  9883  infmap2  10200  cflm  10233  cflim2  10247  hsmex3  10418  domtriomlem  10426  axdc3lem2  10435  brdom7disj  10515  brdom6disj  10516  npex  10971  hashf1lem2  14493  issubc  17892  symgbas  19442  symgbasfi  19449  tgval  23081  ustfn  24328  ustval  24329  ustn0  24347  birthdaylem1  27082  nosupno  27833  rgrprc  29882  wksfval  29900  mptctf  33002  measbase  34532  measval  34533  ismeas  34534  isrnmeas  34535  ballotlem2  34824  subfaclefac  35601  satfvsuclem1  35784  dfon2lem2  36207  poimirlem4  38197  poimirlem9  38202  poimirlem26  38219  poimirlem27  38220  poimirlem28  38221  poimirlem32  38225  sdclem2  38315  lineset  40436  lautset  40780  pautsetN  40796  tendoset  41457  eldiophb  43414  rmxyelqirr  43563  hbtlem1  43776  hbtlem7  43778  relopabVD  45535  rabexgf  45670  prprval  48186  upwlksfval  48823