Theorem ss2abi 4064

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

Syntax hints:   → wi 4  ⊤wtru 1543  {cab 2710   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-in 3956  df-ss 3966

This theorem is referenced by:  abssi  4068  rabssab  4084  abanssl  4302  abanssr  4303  pwpwssunieq  5108  intabs  5343  abssexg  5381  imassrn  6071  fvclss  7241  fabexg  7925  f1oabexg  7927  mapex  8826  f1osetex  8853  fsetexb  8858  tc2  9737  hta  9892  infmap2  10213  cflm  10245  cflim2  10258  hsmex3  10429  domtriomlem  10437  axdc3lem2  10446  brdom7disj  10526  brdom6disj  10527  npex  10981  hashf1lem2  14417  issubc  17785  isghm  19092  permsetexOLD  19237  symgbas  19238  symgbasfi  19246  tgval  22458  ustfn  23706  ustval  23707  ustn0  23725  birthdaylem1  26456  nosupno  27206  rgrprc  28848  wksfval  28866  mptctf  31942  measbase  33195  measval  33196  ismeas  33197  isrnmeas  33198  ballotlem2  33487  subfaclefac  34167  satfvsuclem1  34350  dfon2lem2  34756  poimirlem4  36492  poimirlem9  36497  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem32  36520  sdclem2  36610  lineset  38609  lautset  38953  pautsetN  38969  tendoset  39630  eldiophb  41495  rmxyelqirr  41648  hbtlem1  41865  hbtlem7  41867  relopabVD  43662  rabexgf  43708  prprval  46182  upwlksfval  46513