Theorem ss2abi 4067

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2110, ax-10 2141, ax-11 2157, ax-12 2177. (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 1544	. 2 ⊢ ⊤
2		ss2abi.1	. . . 4 ⊢ (𝜑 → 𝜓)
3	2	a1i 11	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
4	3	ss2abdv 4066	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1541  {cab 2714   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-tru 1543  df-sb 2065  df-clab 2715  df-ss 3968

This theorem is referenced by:  abssi  4070  rabssab  4085  abanssl  4311  abanssr  4312  pwpwssunieq  5104  intabs  5349  abssexg  5382  imassrn  6089  fvclss  7261  fabexgOLD  7961  mapex  7963  f1oabexgOLD  7965  mapexOLD  8872  f1osetex  8899  fsetexb  8904  tc2  9782  hta  9937  infmap2  10257  cflm  10290  cflim2  10303  hsmex3  10474  domtriomlem  10482  axdc3lem2  10491  brdom7disj  10571  brdom6disj  10572  npex  11026  hashf1lem2  14495  issubc  17880  isghmOLD  19234  symgbas  19389  symgbasfi  19396  tgval  22962  ustfn  24210  ustval  24211  ustn0  24229  birthdaylem1  26994  nosupno  27748  rgrprc  29609  wksfval  29627  mptctf  32729  measbase  34198  measval  34199  ismeas  34200  isrnmeas  34201  ballotlem2  34491  subfaclefac  35181  satfvsuclem1  35364  dfon2lem2  35785  poimirlem4  37631  poimirlem9  37636  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem32  37659  sdclem2  37749  lineset  39740  lautset  40084  pautsetN  40100  tendoset  40761  eldiophb  42768  rmxyelqirr  42921  hbtlem1  43135  hbtlem7  43137  relopabVD  44921  rabexgf  45029  prprval  47501  upwlksfval  48051