Theorem ss2abi 4017

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571  {cab 2740   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-ss 3919

This theorem is used by:  abssi  4019  rabssab  4036  abanssl  4260  abanssr  4261  pwpwssunieq  5068  intabs  5317  abssexg  5351  imassrn  6071  fvclss  7242  mapex  7941  f1osetex  8864  fsetexb  8869  tc2  9723  htaOLD  9906  infmap2  10223  cflm  10255  cflim2  10269  hsmex3  10440  domtriomlem  10448  axdc3lem2  10457  brdom7disj  10538  brdom6disj  10539  npex  10999  hashf1lem2  14525  issubc  17930  symgbas  19505  symgbasfi  19512  tgval  23186  ustfn  24434  ustval  24435  ustn0  24453  birthdaylem1  27196  nosupno  27947  rgrprc  30059  wksfval  30077  mptctf  33195  measbase  34716  measval  34717  ismeas  34718  isrnmeas  34719  ballotlem2  35008  subfaclefac  35763  satfvsuclem1  35946  dfon2lem2  36369  poimirlem4  38381  poimirlem9  38386  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem32  38409  sdclem2  38500  lineset  40619  lautset  40963  pautsetN  40979  tendoset  41640  eldiophb  43610  rmxyelqirr  43759  hbtlem1  43972  hbtlem7  43974  relopabVD  45731  rabexgf  45866  prprval  48422  upwlksfval  49059