Theorem ss2abi 3994

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2149, ax-10 2180, ax-11 2197, ax-12 2216. (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 3993	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1577	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

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

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 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-ss 3901

This theorem is used by:  abssi  3996  rabssab  4013  abanssl  4259  abanssr  4260  pwpwssunieq  5067  intabs  5314  abssexg  5348  relopabi  5805  imassrnOLD  6081  fvclss  7268  mapex  7976  f1osetex  8909  fsetexb  8914  tc2  9768  htaOLD  9990  infmap2  10322  cflm  10354  cflim2  10368  hsmex3  10539  domtriomlem  10547  axdc3lem2  10556  brdom7disj  10637  brdom6disj  10638  npex  11098  hashf1lem2  14628  issubc  18039  symgbas  19616  symgbasfi  19623  tgval  23303  ustfn  24551  ustval  24552  ustn0  24570  birthdaylem1  27309  nosupno  28090  rgrprc  30202  wksfval  30220  mptctf  33379  measbase  34900  measval  34901  ismeas  34902  isrnmeas  34903  ballotlem2  35191  abweex  35801  subfaclefac  36108  satfvsuclem1  36291  dfon2lem1  36723  dfon2lem2  36724  poimirlem4  38734  poimirlem9  38739  poimirlem26  38756  poimirlem27  38757  poimirlem28  38758  poimirlem32  38762  sdclem2  38868  lineset  40987  lautset  41331  pautsetN  41347  tendoset  42008  eldiophb  43961  rmxyelqirr  44110  hbtlem1  44317  hbtlem7  44319  relopabVD  46074  rabexgf  46246  prprval  48801  upwlksfval  49438