Theorem ss2abi 4019

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2111, ax-10 2142, ax-11 2158, ax-12 2178. (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 4018	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1541  {cab 2707   ⊆ wss 3903

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 2066  df-clab 2708  df-ss 3920

This theorem is referenced by:  abssi  4021  rabssab  4036  abanssl  4262  abanssr  4263  pwpwssunieq  5053  intabs  5288  abssexg  5321  imassrn  6022  fvclss  7177  fabexgOLD  7872  mapex  7874  f1oabexgOLD  7876  mapexOLD  8759  f1osetex  8786  fsetexb  8791  tc2  9638  hta  9793  infmap2  10111  cflm  10144  cflim2  10157  hsmex3  10328  domtriomlem  10336  axdc3lem2  10345  brdom7disj  10425  brdom6disj  10426  npex  10880  hashf1lem2  14363  issubc  17742  isghmOLD  19095  symgbas  19251  symgbasfi  19258  tgval  22840  ustfn  24087  ustval  24088  ustn0  24106  birthdaylem1  26859  nosupno  27613  rgrprc  29537  wksfval  29555  mptctf  32661  measbase  34170  measval  34171  ismeas  34172  isrnmeas  34173  ballotlem2  34463  subfaclefac  35159  satfvsuclem1  35342  dfon2lem2  35768  poimirlem4  37614  poimirlem9  37619  poimirlem26  37636  poimirlem27  37637  poimirlem28  37638  poimirlem32  37642  sdclem2  37732  lineset  39727  lautset  40071  pautsetN  40087  tendoset  40748  eldiophb  42740  rmxyelqirr  42893  hbtlem1  43106  hbtlem7  43108  relopabVD  44884  rabexgf  45012  prprval  47508  upwlksfval  48129