Theorem ss2abi 4018

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

Syntax hints:   → wi 4  ⊤wtru 1542  {cab 2709   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 207  df-tru 1544  df-sb 2068  df-clab 2710  df-ss 3919

This theorem is referenced by:  abssi  4020  rabssab  4035  abanssl  4261  abanssr  4262  pwpwssunieq  5052  intabs  5287  abssexg  5320  imassrn  6020  fvclss  7175  fabexgOLD  7869  mapex  7871  f1oabexgOLD  7873  mapexOLD  8756  f1osetex  8783  fsetexb  8788  tc2  9632  hta  9787  infmap2  10105  cflm  10138  cflim2  10151  hsmex3  10322  domtriomlem  10330  axdc3lem2  10339  brdom7disj  10419  brdom6disj  10420  npex  10874  hashf1lem2  14360  issubc  17739  isghmOLD  19126  symgbas  19282  symgbasfi  19289  tgval  22868  ustfn  24115  ustval  24116  ustn0  24134  birthdaylem1  26886  nosupno  27640  rgrprc  29568  wksfval  29586  mptctf  32694  measbase  34205  measval  34206  ismeas  34207  isrnmeas  34208  ballotlem2  34497  subfaclefac  35208  satfvsuclem1  35391  dfon2lem2  35817  poimirlem4  37663  poimirlem9  37668  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem32  37691  sdclem2  37781  lineset  39776  lautset  40120  pautsetN  40136  tendoset  40797  eldiophb  42789  rmxyelqirr  42942  hbtlem1  43155  hbtlem7  43157  relopabVD  44932  rabexgf  45060  prprval  47544  upwlksfval  48165