Theorem ss2abi 4033

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 4032	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1541  {cab 2708   ⊆ wss 3917

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 2709  df-ss 3934

This theorem is referenced by:  abssi  4036  rabssab  4051  abanssl  4277  abanssr  4278  pwpwssunieq  5071  intabs  5307  abssexg  5340  imassrn  6045  fvclss  7218  fabexgOLD  7918  mapex  7920  f1oabexgOLD  7922  mapexOLD  8808  f1osetex  8835  fsetexb  8840  tc2  9702  hta  9857  infmap2  10177  cflm  10210  cflim2  10223  hsmex3  10394  domtriomlem  10402  axdc3lem2  10411  brdom7disj  10491  brdom6disj  10492  npex  10946  hashf1lem2  14428  issubc  17804  isghmOLD  19155  symgbas  19309  symgbasfi  19316  tgval  22849  ustfn  24096  ustval  24097  ustn0  24115  birthdaylem1  26868  nosupno  27622  rgrprc  29526  wksfval  29544  mptctf  32648  measbase  34194  measval  34195  ismeas  34196  isrnmeas  34197  ballotlem2  34487  subfaclefac  35170  satfvsuclem1  35353  dfon2lem2  35779  poimirlem4  37625  poimirlem9  37630  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem32  37653  sdclem2  37743  lineset  39739  lautset  40083  pautsetN  40099  tendoset  40760  eldiophb  42752  rmxyelqirr  42905  hbtlem1  43119  hbtlem7  43121  relopabVD  44897  rabexgf  45025  prprval  47519  upwlksfval  48127