Theorem ss2abi 4076

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

Syntax hints:   → wi 4  ⊤wtru 1537  {cab 2711   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-tru 1539  df-sb 2062  df-clab 2712  df-ss 3979

This theorem is referenced by:  abssi  4079  rabssab  4094  abanssl  4316  abanssr  4317  pwpwssunieq  5108  intabs  5354  abssexg  5387  imassrn  6090  fvclss  7260  fabexgOLD  7959  mapex  7961  f1oabexgOLD  7963  mapexOLD  8870  f1osetex  8897  fsetexb  8902  tc2  9779  hta  9934  infmap2  10254  cflm  10287  cflim2  10300  hsmex3  10471  domtriomlem  10479  axdc3lem2  10488  brdom7disj  10568  brdom6disj  10569  npex  11023  hashf1lem2  14491  issubc  17885  isghmOLD  19246  symgbas  19403  symgbasfi  19410  tgval  22977  ustfn  24225  ustval  24226  ustn0  24244  birthdaylem1  27008  nosupno  27762  rgrprc  29623  wksfval  29641  mptctf  32734  measbase  34177  measval  34178  ismeas  34179  isrnmeas  34180  ballotlem2  34469  subfaclefac  35160  satfvsuclem1  35343  dfon2lem2  35765  poimirlem4  37610  poimirlem9  37615  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem32  37638  sdclem2  37728  lineset  39720  lautset  40064  pautsetN  40080  tendoset  40741  eldiophb  42744  rmxyelqirr  42897  hbtlem1  43111  hbtlem7  43113  relopabVD  44898  rabexgf  44961  prprval  47438  upwlksfval  47978