Theorem ss2abi 4021

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

Syntax hints:   → wi 4  ⊤wtru 1571  {cab 2741   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-ss 3923

This theorem is referenced by:  abssi  4023  rabssab  4040  abanssl  4265  abanssr  4266  pwpwssunieq  5071  intabs  5321  abssexg  5355  imassrn  6075  fvclss  7241  mapex  7938  f1osetex  8857  fsetexb  8862  tc2  9710  hta  9884  infmap2  10201  cflm  10234  cflim2  10248  hsmex3  10419  domtriomlem  10427  axdc3lem2  10436  brdom7disj  10516  brdom6disj  10517  npex  10972  hashf1lem2  14495  issubc  17893  symgbas  19443  symgbasfi  19450  tgval  23093  ustfn  24340  ustval  24341  ustn0  24359  birthdaylem1  27094  nosupno  27845  rgrprc  29919  wksfval  29937  mptctf  33039  measbase  34565  measval  34566  ismeas  34567  isrnmeas  34568  ballotlem2  34857  subfaclefac  35646  satfvsuclem1  35829  dfon2lem2  36252  poimirlem4  38253  poimirlem9  38258  poimirlem26  38275  poimirlem27  38276  poimirlem28  38277  poimirlem32  38281  sdclem2  38371  lineset  40490  lautset  40834  pautsetN  40850  tendoset  41511  eldiophb  43468  rmxyelqirr  43617  hbtlem1  43830  hbtlem7  43832  relopabVD  45589  rabexgf  45724  prprval  48240  upwlksfval  48877