Theorem ss2abi 4062

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2101, ax-10 2130, ax-11 2147, ax-12 2167. (Revised by GG, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abi.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ss2abi

Step	Hyp	Ref	Expression
1		tru 1538	. 2 ⊢ ⊤
2		ss2abi.1	. . . 4 ⊢ (𝜑 → 𝜓)
3	2	a1i 11	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
4	3	ss2abdv 4060	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1535  {cab 2703   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-tru 1537  df-sb 2061  df-clab 2704  df-ss 3964

This theorem is referenced by:  abssi  4066  rabssab  4082  abanssl  4303  abanssr  4304  pwpwssunieq  5112  intabs  5349  abssexg  5386  imassrn  6080  fvclss  7256  fabexgOLD  7950  mapex  7952  f1oabexgOLD  7954  mapexOLD  8861  f1osetex  8888  fsetexb  8893  tc2  9785  hta  9940  infmap2  10261  cflm  10293  cflim2  10306  hsmex3  10477  domtriomlem  10485  axdc3lem2  10494  brdom7disj  10574  brdom6disj  10575  npex  11029  hashf1lem2  14475  issubc  17854  isghmOLD  19210  permsetexOLD  19367  symgbas  19368  symgbasfi  19376  tgval  22949  ustfn  24197  ustval  24198  ustn0  24216  birthdaylem1  26979  nosupno  27733  rgrprc  29528  wksfval  29546  mptctf  32631  measbase  34030  measval  34031  ismeas  34032  isrnmeas  34033  ballotlem2  34322  subfaclefac  35004  satfvsuclem1  35187  dfon2lem2  35608  poimirlem4  37325  poimirlem9  37330  poimirlem26  37347  poimirlem27  37348  poimirlem28  37349  poimirlem32  37353  sdclem2  37443  lineset  39437  lautset  39781  pautsetN  39797  tendoset  40458  eldiophb  42414  rmxyelqirr  42567  hbtlem1  42784  hbtlem7  42786  relopabVD  44577  rabexgf  44623  prprval  47086  upwlksfval  47512