Theorem ss2abi 4022

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2147, ax-10 2178, ax-11 2194, ax-12 2215. (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 4021	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1570	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1564  {cab 2743   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-sb 2094  df-clab 2744  df-ss 3924

This theorem is referenced by:  abssi  4024  rabssab  4041  abanssl  4266  abanssr  4267  pwpwssunieq  5066  intabs  5310  abssexg  5344  imassrn  6064  fvclss  7229  mapex  7925  f1osetex  8844  fsetexb  8849  tc2  9697  hta  9871  infmap2  10188  cflm  10221  cflim2  10235  hsmex3  10406  domtriomlem  10414  axdc3lem2  10423  brdom7disj  10503  brdom6disj  10504  npex  10959  hashf1lem2  14483  issubc  17882  symgbas  19433  symgbasfi  19440  tgval  23073  ustfn  24320  ustval  24321  ustn0  24339  birthdaylem1  27074  nosupno  27825  rgrprc  29850  wksfval  29868  mptctf  32973  measbase  34504  measval  34505  ismeas  34506  isrnmeas  34507  ballotlem2  34796  subfaclefac  35539  satfvsuclem1  35722  dfon2lem2  36145  poimirlem4  38135  poimirlem9  38140  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  poimirlem32  38163  sdclem2  38253  lineset  40374  lautset  40718  pautsetN  40734  tendoset  41395  eldiophb  43350  rmxyelqirr  43499  hbtlem1  43712  hbtlem7  43714  relopabVD  45474  rabexgf  45602  prprval  48118  upwlksfval  48755