Theorem ss2abi 4090

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

Syntax hints:   → wi 4  ⊤wtru 1538  {cab 2717   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-tru 1540  df-sb 2065  df-clab 2718  df-ss 3993

This theorem is referenced by:  abssi  4093  rabssab  4108  abanssl  4330  abanssr  4331  pwpwssunieq  5127  intabs  5367  abssexg  5400  imassrn  6100  fvclss  7278  fabexgOLD  7977  mapex  7979  f1oabexgOLD  7981  mapexOLD  8890  f1osetex  8917  fsetexb  8922  tc2  9811  hta  9966  infmap2  10286  cflm  10319  cflim2  10332  hsmex3  10503  domtriomlem  10511  axdc3lem2  10520  brdom7disj  10600  brdom6disj  10601  npex  11055  hashf1lem2  14505  issubc  17899  isghmOLD  19256  symgbas  19413  symgbasfi  19420  tgval  22983  ustfn  24231  ustval  24232  ustn0  24250  birthdaylem1  27012  nosupno  27766  rgrprc  29627  wksfval  29645  mptctf  32731  measbase  34161  measval  34162  ismeas  34163  isrnmeas  34164  ballotlem2  34453  subfaclefac  35144  satfvsuclem1  35327  dfon2lem2  35748  poimirlem4  37584  poimirlem9  37589  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem32  37612  sdclem2  37702  lineset  39695  lautset  40039  pautsetN  40055  tendoset  40716  eldiophb  42713  rmxyelqirr  42866  hbtlem1  43080  hbtlem7  43082  relopabVD  44872  rabexgf  44924  prprval  47388  upwlksfval  47858