Theorem ss2abi 4014

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2147, ax-10 2178, ax-11 2194, ax-12 2213. (Revised by GG, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ss2abi	⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Proof of Theorem ss2abi

Step	Hyp	Ref	Expression
1		ss2abi.1	. . . 4 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
3	2	ss2abdv 4013	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1577	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571  {cab 2739   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-ss 3916

This theorem is used by:  abssi  4016  rabssab  4033  abanssl  4257  abanssr  4258  pwpwssunieq  5064  intabs  5310  abssexg  5344  imassrn  6065  fvclss  7237  mapex  7941  f1osetex  8865  fsetexb  8870  tc2  9725  htaOLD  9944  infmap2  10276  cflm  10308  cflim2  10322  hsmex3  10493  domtriomlem  10501  axdc3lem2  10510  brdom7disj  10591  brdom6disj  10592  npex  11052  hashf1lem2  14581  issubc  17990  symgbas  19566  symgbasfi  19573  tgval  23253  ustfn  24501  ustval  24502  ustn0  24520  birthdaylem1  27261  nosupno  28042  rgrprc  30154  wksfval  30172  mptctf  33290  measbase  34812  measval  34813  ismeas  34814  isrnmeas  34815  ballotlem2  35104  subfaclefac  35910  satfvsuclem1  36093  dfon2lem2  36516  poimirlem4  38510  poimirlem9  38515  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  poimirlem32  38538  sdclem2  38644  lineset  40763  lautset  41107  pautsetN  41123  tendoset  41784  eldiophb  43721  rmxyelqirr  43870  hbtlem1  44083  hbtlem7  44085  relopabVD  45842  rabexgf  45984  prprval  48540  upwlksfval  49177