Theorem ss2abi 4015

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2115, ax-10 2146, ax-11 2162, ax-12 2182. (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 1545	. 2 ⊢ ⊤
2		ss2abi.1	. . . 4 ⊢ (𝜑 → 𝜓)
3	2	a1i 11	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
4	3	ss2abdv 4014	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1542  {cab 2711   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-ss 3915

This theorem is referenced by:  abssi  4017  rabssab  4034  abanssl  4260  abanssr  4261  pwpwssunieq  5054  intabs  5289  abssexg  5322  imassrn  6024  fvclss  7181  fabexgOLD  7875  mapex  7877  f1oabexgOLD  7879  mapexOLD  8762  f1osetex  8789  fsetexb  8794  tc2  9637  hta  9797  infmap2  10115  cflm  10148  cflim2  10161  hsmex3  10332  domtriomlem  10340  axdc3lem2  10349  brdom7disj  10429  brdom6disj  10430  npex  10884  hashf1lem2  14365  issubc  17744  isghmOLD  19130  symgbas  19286  symgbasfi  19293  tgval  22871  ustfn  24118  ustval  24119  ustn0  24137  birthdaylem1  26889  nosupno  27643  rgrprc  29572  wksfval  29590  mptctf  32703  measbase  34231  measval  34232  ismeas  34233  isrnmeas  34234  ballotlem2  34523  subfaclefac  35241  satfvsuclem1  35424  dfon2lem2  35847  poimirlem4  37684  poimirlem9  37689  poimirlem26  37706  poimirlem27  37707  poimirlem28  37708  poimirlem32  37712  sdclem2  37802  lineset  39857  lautset  40201  pautsetN  40217  tendoset  40878  eldiophb  42874  rmxyelqirr  43027  hbtlem1  43240  hbtlem7  43242  relopabVD  45017  rabexgf  45145  prprval  47638  upwlksfval  48259