Theorem ss2abi 3996

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

Syntax hints:   → wi 4  ⊤wtru 1540  {cab 2715   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-in 3890  df-ss 3900

This theorem is referenced by:  abssi  3999  rabssab  4014  abanssl  4232  abanssr  4233  pwpwssunieq  5029  intabs  5261  abssexg  5300  imassrn  5969  fvclss  7097  fabexg  7755  f1oabexg  7757  mapex  8579  f1osetex  8605  fsetexb  8610  tc2  9431  hta  9586  infmap2  9905  cflm  9937  cflim2  9950  hsmex3  10121  domtriomlem  10129  axdc3lem2  10138  brdom7disj  10218  brdom6disj  10219  npex  10673  hashf1lem2  14098  issubc  17466  isghm  18749  permsetexOLD  18892  symgbas  18893  symgbasfi  18901  tgval  22013  ustfn  23261  ustval  23262  ustn0  23280  birthdaylem1  26006  rgrprc  27861  wksfval  27879  mptctf  30954  measbase  32065  measval  32066  ismeas  32067  isrnmeas  32068  ballotlem2  32355  subfaclefac  33038  satfvsuclem1  33221  dfon2lem2  33666  nosupno  33833  poimirlem4  35708  poimirlem9  35713  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem32  35736  sdclem2  35827  lineset  37679  lautset  38023  pautsetN  38039  tendoset  38700  eldiophb  40495  hbtlem1  40864  hbtlem7  40866  relopabVD  42410  rabexgf  42456  prprval  44854  upwlksfval  45185