Theorem ss2abi 4007

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

Syntax hints:   → wi 4  ⊤wtru 1543  {cab 2715   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-ss 3907

This theorem is referenced by:  abssi  4009  rabssab  4026  abanssl  4252  abanssr  4253  pwpwssunieq  5047  intabs  5286  abssexg  5319  imassrn  6030  fvclss  7189  fabexgOLD  7883  mapex  7885  f1oabexgOLD  7887  mapexOLD  8772  f1osetex  8799  fsetexb  8804  tc2  9652  hta  9812  infmap2  10130  cflm  10163  cflim2  10176  hsmex3  10347  domtriomlem  10355  axdc3lem2  10364  brdom7disj  10444  brdom6disj  10445  npex  10900  hashf1lem2  14409  issubc  17793  isghmOLD  19182  symgbas  19338  symgbasfi  19345  tgval  22930  ustfn  24177  ustval  24178  ustn0  24196  birthdaylem1  26928  nosupno  27681  rgrprc  29675  wksfval  29693  mptctf  32804  measbase  34357  measval  34358  ismeas  34359  isrnmeas  34360  ballotlem2  34649  subfaclefac  35374  satfvsuclem1  35557  dfon2lem2  35980  poimirlem4  37959  poimirlem9  37964  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem32  37987  sdclem2  38077  lineset  40198  lautset  40542  pautsetN  40558  tendoset  41219  eldiophb  43203  rmxyelqirr  43356  hbtlem1  43569  hbtlem7  43571  relopabVD  45345  rabexgf  45473  prprval  47986  upwlksfval  48623