Theorem ss2abi 4062

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2108, ax-10 2137, ax-11 2154, ax-12 2171. (Revised by Gino Giotto, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abi.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ss2abi

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

Syntax hints:   → wi 4  ⊤wtru 1542  {cab 2709   ⊆ wss 3947

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-in 3954  df-ss 3964

This theorem is referenced by:  abssi  4066  rabssab  4082  abanssl  4300  abanssr  4301  pwpwssunieq  5106  intabs  5341  abssexg  5379  imassrn  6068  fvclss  7237  fabexg  7921  f1oabexg  7923  mapex  8822  f1osetex  8849  fsetexb  8854  tc2  9733  hta  9888  infmap2  10209  cflm  10241  cflim2  10254  hsmex3  10425  domtriomlem  10433  axdc3lem2  10442  brdom7disj  10522  brdom6disj  10523  npex  10977  hashf1lem2  14413  issubc  17781  isghm  19086  permsetexOLD  19231  symgbas  19232  symgbasfi  19240  tgval  22449  ustfn  23697  ustval  23698  ustn0  23716  birthdaylem1  26445  nosupno  27195  rgrprc  28837  wksfval  28855  mptctf  31929  measbase  33183  measval  33184  ismeas  33185  isrnmeas  33186  ballotlem2  33475  subfaclefac  34155  satfvsuclem1  34338  dfon2lem2  34744  poimirlem4  36480  poimirlem9  36485  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  poimirlem32  36508  sdclem2  36598  lineset  38597  lautset  38941  pautsetN  38957  tendoset  39618  eldiophb  41480  rmxyelqirr  41633  hbtlem1  41850  hbtlem7  41852  relopabVD  43647  rabexgf  43693  prprval  46168  upwlksfval  46499