Theorem ss2abi 4030

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2111, ax-10 2142, ax-11 2158, ax-12 2178. (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 4029	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1541  {cab 2707   ⊆ wss 3914

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 2066  df-clab 2708  df-ss 3931

This theorem is referenced by:  abssi  4033  rabssab  4048  abanssl  4274  abanssr  4275  pwpwssunieq  5068  intabs  5304  abssexg  5337  imassrn  6042  fvclss  7215  fabexgOLD  7915  mapex  7917  f1oabexgOLD  7919  mapexOLD  8805  f1osetex  8832  fsetexb  8837  tc2  9695  hta  9850  infmap2  10170  cflm  10203  cflim2  10216  hsmex3  10387  domtriomlem  10395  axdc3lem2  10404  brdom7disj  10484  brdom6disj  10485  npex  10939  hashf1lem2  14421  issubc  17797  isghmOLD  19148  symgbas  19302  symgbasfi  19309  tgval  22842  ustfn  24089  ustval  24090  ustn0  24108  birthdaylem1  26861  nosupno  27615  rgrprc  29519  wksfval  29537  mptctf  32641  measbase  34187  measval  34188  ismeas  34189  isrnmeas  34190  ballotlem2  34480  subfaclefac  35163  satfvsuclem1  35346  dfon2lem2  35772  poimirlem4  37618  poimirlem9  37623  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem32  37646  sdclem2  37736  lineset  39732  lautset  40076  pautsetN  40092  tendoset  40753  eldiophb  42745  rmxyelqirr  42898  hbtlem1  43112  hbtlem7  43114  relopabVD  44890  rabexgf  45018  prprval  47515  upwlksfval  48123