Theorem ss2abi 4019

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2143, ax-10 2174, ax-11 2190, ax-12 2211. (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 4018	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
4	3	mptru 1566	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1560  {cab 2739   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-sb 2090  df-clab 2740  df-ss 3921

This theorem is referenced by:  abssi  4021  rabssab  4038  abanssl  4263  abanssr  4264  pwpwssunieq  5060  intabs  5304  abssexg  5338  imassrn  6057  fvclss  7221  mapex  7917  mapexOLD  8809  f1osetex  8836  fsetexb  8841  tc2  9692  hta  9852  infmap2  10170  cflm  10203  cflim2  10217  hsmex3  10388  domtriomlem  10396  axdc3lem2  10405  brdom7disj  10485  brdom6disj  10486  npex  10941  hashf1lem2  14466  issubc  17851  symgbas  19395  symgbasfi  19402  tgval  22995  ustfn  24242  ustval  24243  ustn0  24261  birthdaylem1  26993  nosupno  27744  rgrprc  29738  wksfval  29756  mptctf  32868  measbase  34455  measval  34456  ismeas  34457  isrnmeas  34458  ballotlem2  34747  subfaclefac  35490  satfvsuclem1  35673  dfon2lem2  36096  poimirlem4  38087  poimirlem9  38092  poimirlem26  38109  poimirlem27  38110  poimirlem28  38111  poimirlem32  38115  sdclem2  38205  lineset  40326  lautset  40670  pautsetN  40686  tendoset  41347  eldiophb  43302  rmxyelqirr  43451  hbtlem1  43664  hbtlem7  43666  relopabVD  45440  rabexgf  45568  prprval  48084  upwlksfval  48721