Theorem ss2abi 4004

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2121, ax-10 2152, ax-11 2168, ax-12 2189. (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 4003	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1554	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1548  {cab 2718   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-ss 3907

This theorem is referenced by:  abssi  4006  rabssab  4023  abanssl  4246  abanssr  4247  pwpwssunieq  5040  intabs  5284  abssexg  5318  imassrn  6030  fvclss  7192  fabexgOLD  7886  mapex  7888  f1oabexgOLD  7890  mapexOLD  8776  f1osetex  8803  fsetexb  8808  tc2  9659  hta  9819  infmap2  10137  cflm  10170  cflim2  10183  hsmex3  10354  domtriomlem  10362  axdc3lem2  10371  brdom7disj  10451  brdom6disj  10452  npex  10907  hashf1lem2  14416  issubc  17800  isghmOLD  19189  symgbas  19345  symgbasfi  19352  tgval  22945  ustfn  24192  ustval  24193  ustn0  24211  birthdaylem1  26940  nosupno  27692  rgrprc  29685  wksfval  29703  mptctf  32815  measbase  34388  measval  34389  ismeas  34390  isrnmeas  34391  ballotlem2  34680  subfaclefac  35411  satfvsuclem1  35594  dfon2lem2  36017  poimirlem4  37998  poimirlem9  38003  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  poimirlem32  38026  sdclem2  38116  lineset  40237  lautset  40581  pautsetN  40597  tendoset  41258  eldiophb  43213  rmxyelqirr  43362  hbtlem1  43575  hbtlem7  43577  relopabVD  45351  rabexgf  45479  prprval  47996  upwlksfval  48633