Theorem ss2abi 4021

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

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

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 3922

This theorem is referenced by:  abssi  4023  rabssab  4038  abanssl  4264  abanssr  4265  pwpwssunieq  5056  intabs  5291  abssexg  5324  imassrn  6026  fvclss  7181  fabexgOLD  7879  mapex  7881  f1oabexgOLD  7883  mapexOLD  8766  f1osetex  8793  fsetexb  8798  tc2  9657  hta  9812  infmap2  10130  cflm  10163  cflim2  10176  hsmex3  10347  domtriomlem  10355  axdc3lem2  10364  brdom7disj  10444  brdom6disj  10445  npex  10899  hashf1lem2  14381  issubc  17760  isghmOLD  19113  symgbas  19269  symgbasfi  19276  tgval  22858  ustfn  24105  ustval  24106  ustn0  24124  birthdaylem1  26877  nosupno  27631  rgrprc  29555  wksfval  29573  mptctf  32674  measbase  34163  measval  34164  ismeas  34165  isrnmeas  34166  ballotlem2  34456  subfaclefac  35148  satfvsuclem1  35331  dfon2lem2  35757  poimirlem4  37603  poimirlem9  37608  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  poimirlem32  37631  sdclem2  37721  lineset  39717  lautset  40061  pautsetN  40077  tendoset  40738  eldiophb  42730  rmxyelqirr  42883  hbtlem1  43096  hbtlem7  43098  relopabVD  44874  rabexgf  45002  prprval  47499  upwlksfval  48120