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  28879  wksfval  28897  mptctf  31973  measbase  33226  measval  33227  ismeas  33228  isrnmeas  33229  ballotlem2  33518  subfaclefac  34198  satfvsuclem1  34381  dfon2lem2  34787  poimirlem4  36540  poimirlem9  36545  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  poimirlem32  36568  sdclem2  36658  lineset  38657  lautset  39001  pautsetN  39017  tendoset  39678  eldiophb  41543  rmxyelqirr  41696  hbtlem1  41913  hbtlem7  41915  relopabVD  43710  rabexgf  43756  prprval  46230  upwlksfval  46561