Theorem ss2abi 4011

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

Syntax hints:   → wi 4  ⊤wtru 1541  {cab 2713   ⊆ wss 3898

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-in 3905  df-ss 3915

This theorem is referenced by:  abssi  4015  rabssab  4030  abanssl  4248  abanssr  4249  pwpwssunieq  5051  intabs  5286  abssexg  5325  imassrn  6010  fvclss  7171  fabexg  7849  f1oabexg  7851  mapex  8692  f1osetex  8718  fsetexb  8723  tc2  9599  hta  9754  infmap2  10075  cflm  10107  cflim2  10120  hsmex3  10291  domtriomlem  10299  axdc3lem2  10308  brdom7disj  10388  brdom6disj  10389  npex  10843  hashf1lem2  14270  issubc  17647  isghm  18930  permsetexOLD  19073  symgbas  19074  symgbasfi  19082  tgval  22211  ustfn  23459  ustval  23460  ustn0  23478  birthdaylem1  26207  nosupno  26957  rgrprc  28247  wksfval  28265  mptctf  31339  measbase  32463  measval  32464  ismeas  32465  isrnmeas  32466  ballotlem2  32755  subfaclefac  33437  satfvsuclem1  33620  dfon2lem2  34043  poimirlem4  35894  poimirlem9  35899  poimirlem26  35916  poimirlem27  35917  poimirlem28  35918  poimirlem32  35922  sdclem2  36013  lineset  38014  lautset  38358  pautsetN  38374  tendoset  39035  eldiophb  40849  rmxyelqirr  41002  hbtlem1  41219  hbtlem7  41221  relopabVD  42850  rabexgf  42896  prprval  45325  upwlksfval  45656