Theorem ss2abi 4020

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

Syntax hints:   → wi 4  ⊤wtru 1543  {cab 2715   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-ss 3920

This theorem is referenced by:  abssi  4022  rabssab  4039  abanssl  4265  abanssr  4266  pwpwssunieq  5061  intabs  5296  abssexg  5329  imassrn  6038  fvclss  7197  fabexgOLD  7891  mapex  7893  f1oabexgOLD  7895  mapexOLD  8781  f1osetex  8808  fsetexb  8813  tc2  9661  hta  9821  infmap2  10139  cflm  10172  cflim2  10185  hsmex3  10356  domtriomlem  10364  axdc3lem2  10373  brdom7disj  10453  brdom6disj  10454  npex  10909  hashf1lem2  14391  issubc  17771  isghmOLD  19157  symgbas  19313  symgbasfi  19320  tgval  22911  ustfn  24158  ustval  24159  ustn0  24177  birthdaylem1  26929  nosupno  27683  rgrprc  29677  wksfval  29695  mptctf  32805  measbase  34374  measval  34375  ismeas  34376  isrnmeas  34377  ballotlem2  34666  subfaclefac  35389  satfvsuclem1  35572  dfon2lem2  35995  poimirlem4  37869  poimirlem9  37874  poimirlem26  37891  poimirlem27  37892  poimirlem28  37893  poimirlem32  37897  sdclem2  37987  lineset  40108  lautset  40452  pautsetN  40468  tendoset  41129  eldiophb  43108  rmxyelqirr  43261  hbtlem1  43474  hbtlem7  43476  relopabVD  45250  rabexgf  45378  prprval  47868  upwlksfval  48489