Theorem ss2abi 3994

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

Syntax hints:   → wi 4  ⊤wtru 1539  {cab 2776   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-in 3888  df-ss 3898

This theorem is referenced by:  abssi  3997  rabssab  4011  pwpwssunieq  4989  intabs  5209  abssexg  5248  imassrn  5907  fvclss  6979  fabexg  7621  f1oabexg  7624  mapex  8395  tc2  9168  hta  9310  infmap2  9629  cflm  9661  cflim2  9674  hsmex3  9845  domtriomlem  9853  axdc3lem2  9862  brdom7disj  9942  brdom6disj  9943  npex  10397  hashf1lem2  13810  issubc  17097  isghm  18350  permsetex  18490  symgbas  18491  symgbasfi  18499  tgval  21560  ustfn  22807  ustval  22808  ustn0  22826  birthdaylem1  25537  rgrprc  27381  wksfval  27399  mptctf  30479  measbase  31566  measval  31567  ismeas  31568  isrnmeas  31569  ballotlem2  31856  subfaclefac  32536  satfvsuclem1  32719  dfon2lem2  33142  nosupno  33316  poimirlem4  35061  poimirlem9  35066  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem32  35089  sdclem2  35180  lineset  37034  lautset  37378  pautsetN  37394  tendoset  38055  eldiophb  39698  hbtlem1  40067  hbtlem7  40069  relopabVD  41607  rabexgf  41653  prprval  44031  upwlksfval  44363