Theorem ss2abi 4001

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2109, ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ss2abi	⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Proof of Theorem ss2abi

Step	Hyp	Ref	Expression
1		tru 1543	. 2 ⊢ ⊤
2		ss2abi.1	. . . 4 ⊢ (𝜑 → 𝜓)
3	2	a1i 11	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
4	3	ss2abdv 3998	. 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1540  {cab 2716   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-in 3895  df-ss 3905

This theorem is referenced by:  abssi  4004  rabssab  4019  abanssl  4236  abanssr  4237  pwpwssunieq  5034  intabs  5267  abssexg  5306  imassrn  5983  fvclss  7124  fabexg  7790  f1oabexg  7792  mapex  8630  f1osetex  8656  fsetexb  8661  tc2  9509  hta  9664  infmap2  9983  cflm  10015  cflim2  10028  hsmex3  10199  domtriomlem  10207  axdc3lem2  10216  brdom7disj  10296  brdom6disj  10297  npex  10751  hashf1lem2  14179  issubc  17559  isghm  18843  permsetexOLD  18986  symgbas  18987  symgbasfi  18995  tgval  22114  ustfn  23362  ustval  23363  ustn0  23381  birthdaylem1  26110  rgrprc  27967  wksfval  27985  mptctf  31061  measbase  32174  measval  32175  ismeas  32176  isrnmeas  32177  ballotlem2  32464  subfaclefac  33147  satfvsuclem1  33330  dfon2lem2  33769  nosupno  33915  poimirlem4  35790  poimirlem9  35795  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem32  35818  sdclem2  35909  lineset  37759  lautset  38103  pautsetN  38119  tendoset  38780  eldiophb  40586  hbtlem1  40955  hbtlem7  40957  relopabVD  42528  rabexgf  42574  prprval  44977  upwlksfval  45308