Theorem ss2abi 4023

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2148, ax-10 2179, ax-11 2195, ax-12 2216. (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 4022	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1577	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571  {cab 2744   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-ss 3925

This theorem is used by:  abssi  4025  rabssab  4042  abanssl  4267  abanssr  4268  pwpwssunieq  5075  intabs  5324  abssexg  5358  imassrn  6078  fvclss  7246  mapex  7946  f1osetex  8865  fsetexb  8870  tc2  9719  htaOLD  9902  infmap2  10219  cflm  10251  cflim2  10265  hsmex3  10436  domtriomlem  10444  axdc3lem2  10453  brdom7disj  10533  brdom6disj  10534  npex  10989  hashf1lem2  14513  issubc  17917  symgbas  19473  symgbasfi  19480  tgval  23149  ustfn  24396  ustval  24397  ustn0  24415  birthdaylem1  27153  nosupno  27904  rgrprc  29978  wksfval  29996  mptctf  33098  measbase  34619  measval  34620  ismeas  34621  isrnmeas  34622  ballotlem2  34911  subfaclefac  35689  satfvsuclem1  35872  dfon2lem2  36295  poimirlem4  38316  poimirlem9  38321  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  poimirlem32  38344  sdclem2  38434  lineset  40553  lautset  40897  pautsetN  40913  tendoset  41574  eldiophb  43529  rmxyelqirr  43678  hbtlem1  43891  hbtlem7  43893  relopabVD  45650  rabexgf  45785  prprval  48304  upwlksfval  48941