Theorem ss2abi 4042

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

Syntax hints:   → wi 4  ⊤wtru 1541  {cab 2713   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-tru 1543  df-sb 2065  df-clab 2714  df-ss 3943

This theorem is referenced by:  abssi  4045  rabssab  4060  abanssl  4286  abanssr  4287  pwpwssunieq  5080  intabs  5319  abssexg  5352  imassrn  6058  fvclss  7233  fabexgOLD  7935  mapex  7937  f1oabexgOLD  7939  mapexOLD  8846  f1osetex  8873  fsetexb  8878  tc2  9756  hta  9911  infmap2  10231  cflm  10264  cflim2  10277  hsmex3  10448  domtriomlem  10456  axdc3lem2  10465  brdom7disj  10545  brdom6disj  10546  npex  11000  hashf1lem2  14474  issubc  17848  isghmOLD  19199  symgbas  19353  symgbasfi  19360  tgval  22893  ustfn  24140  ustval  24141  ustn0  24159  birthdaylem1  26913  nosupno  27667  rgrprc  29571  wksfval  29589  mptctf  32695  measbase  34228  measval  34229  ismeas  34230  isrnmeas  34231  ballotlem2  34521  subfaclefac  35198  satfvsuclem1  35381  dfon2lem2  35802  poimirlem4  37648  poimirlem9  37653  poimirlem26  37670  poimirlem27  37671  poimirlem28  37672  poimirlem32  37676  sdclem2  37766  lineset  39757  lautset  40101  pautsetN  40117  tendoset  40778  eldiophb  42780  rmxyelqirr  42933  hbtlem1  43147  hbtlem7  43149  relopabVD  44925  rabexgf  45048  prprval  47528  upwlksfval  48110