Theorem ss2abi 4018

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

Syntax hints:   → wi 4  ⊤wtru 1542  {cab 2714   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-ss 3918

This theorem is referenced by:  abssi  4020  rabssab  4037  abanssl  4263  abanssr  4264  pwpwssunieq  5059  intabs  5294  abssexg  5327  imassrn  6030  fvclss  7187  fabexgOLD  7881  mapex  7883  f1oabexgOLD  7885  mapexOLD  8769  f1osetex  8796  fsetexb  8801  tc2  9649  hta  9809  infmap2  10127  cflm  10160  cflim2  10173  hsmex3  10344  domtriomlem  10352  axdc3lem2  10361  brdom7disj  10441  brdom6disj  10442  npex  10897  hashf1lem2  14379  issubc  17759  isghmOLD  19145  symgbas  19301  symgbasfi  19308  tgval  22899  ustfn  24146  ustval  24147  ustn0  24165  birthdaylem1  26917  nosupno  27671  rgrprc  29665  wksfval  29683  mptctf  32795  measbase  34354  measval  34355  ismeas  34356  isrnmeas  34357  ballotlem2  34646  subfaclefac  35370  satfvsuclem1  35553  dfon2lem2  35976  poimirlem4  37821  poimirlem9  37826  poimirlem26  37843  poimirlem27  37844  poimirlem28  37845  poimirlem32  37849  sdclem2  37939  lineset  39994  lautset  40338  pautsetN  40354  tendoset  41015  eldiophb  42995  rmxyelqirr  43148  hbtlem1  43361  hbtlem7  43363  relopabVD  45137  rabexgf  45265  prprval  47756  upwlksfval  48377