Theorem ss2abi 4006

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2116, ax-10 2147, ax-11 2163, ax-12 2185. (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 4005	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1549	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1543  {cab 2714   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-ss 3906

This theorem is referenced by:  abssi  4008  rabssab  4025  abanssl  4251  abanssr  4252  pwpwssunieq  5046  intabs  5290  abssexg  5324  imassrn  6036  fvclss  7196  fabexgOLD  7890  mapex  7892  f1oabexgOLD  7894  mapexOLD  8779  f1osetex  8806  fsetexb  8811  tc2  9661  hta  9821  infmap2  10139  cflm  10172  cflim2  10185  hsmex3  10356  domtriomlem  10364  axdc3lem2  10373  brdom7disj  10453  brdom6disj  10454  npex  10909  hashf1lem2  14418  issubc  17802  isghmOLD  19191  symgbas  19347  symgbasfi  19354  tgval  22920  ustfn  24167  ustval  24168  ustn0  24186  birthdaylem1  26915  nosupno  27667  rgrprc  29660  wksfval  29678  mptctf  32789  measbase  34341  measval  34342  ismeas  34343  isrnmeas  34344  ballotlem2  34633  subfaclefac  35358  satfvsuclem1  35541  dfon2lem2  35964  poimirlem4  37945  poimirlem9  37950  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem32  37973  sdclem2  38063  lineset  40184  lautset  40528  pautsetN  40544  tendoset  41205  eldiophb  43189  rmxyelqirr  43338  hbtlem1  43551  hbtlem7  43553  relopabVD  45327  rabexgf  45455  prprval  47974  upwlksfval  48611