Theorem ss2abi 3991

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2146, ax-10 2177, ax-11 2193, ax-12 2212. (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 3990	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1576	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1570  {cab 2738   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-ss 3896

This theorem is used by:  abssi  3993  rabssab  4010  abanssl  4256  abanssr  4257  pwpwssunieq  5063  intabs  5309  abssexg  5343  imassrnOLD  6068  fvclss  7245  mapex  7952  f1osetex  8884  fsetexb  8889  tc2  9744  htaOLD  9966  infmap2  10298  cflm  10330  cflim2  10344  hsmex3  10515  domtriomlem  10523  axdc3lem2  10532  brdom7disj  10613  brdom6disj  10614  npex  11074  hashf1lem2  14604  issubc  18015  symgbas  19591  symgbasfi  19598  tgval  23278  ustfn  24526  ustval  24527  ustn0  24545  birthdaylem1  27284  nosupno  28065  rgrprc  30177  wksfval  30195  mptctf  33355  measbase  34876  measval  34877  ismeas  34878  isrnmeas  34879  ballotlem2  35167  abweex  35769  subfaclefac  36027  satfvsuclem1  36210  dfon2lem1  36637  dfon2lem2  36638  poimirlem4  38635  poimirlem9  38640  poimirlem26  38657  poimirlem27  38658  poimirlem28  38659  poimirlem32  38663  sdclem2  38769  lineset  40888  lautset  41232  pautsetN  41248  tendoset  41909  eldiophb  43861  rmxyelqirr  44010  hbtlem1  44218  hbtlem7  44220  relopabVD  45976  rabexgf  46134  prprval  48689  upwlksfval  49326