MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2abi Structured version   Visualization version   GIF version

Theorem ss2abi 4062
Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2101, ax-10 2130, ax-11 2147, ax-12 2167. (Revised by GG, 28-Jun-2024.)
Hypothesis
Ref Expression
ss2abi.1 (𝜑𝜓)
Assertion
Ref Expression
ss2abi {𝑥𝜑} ⊆ {𝑥𝜓}

Proof of Theorem ss2abi
StepHypRef Expression
1 tru 1538 . 2
2 ss2abi.1 . . . 4 (𝜑𝜓)
32a1i 11 . . 3 (⊤ → (𝜑𝜓))
43ss2abdv 4060 . 2 (⊤ → {𝑥𝜑} ⊆ {𝑥𝜓})
51, 4ax-mp 5 1 {𝑥𝜑} ⊆ {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1535  {cab 2703  wss 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-tru 1537  df-sb 2061  df-clab 2704  df-ss 3964
This theorem is referenced by:  abssi  4066  rabssab  4082  abanssl  4303  abanssr  4304  pwpwssunieq  5112  intabs  5349  abssexg  5386  imassrn  6080  fvclss  7256  fabexgOLD  7950  mapex  7952  f1oabexgOLD  7954  mapexOLD  8861  f1osetex  8888  fsetexb  8893  tc2  9785  hta  9940  infmap2  10261  cflm  10293  cflim2  10306  hsmex3  10477  domtriomlem  10485  axdc3lem2  10494  brdom7disj  10574  brdom6disj  10575  npex  11029  hashf1lem2  14475  issubc  17854  isghmOLD  19210  permsetexOLD  19367  symgbas  19368  symgbasfi  19376  tgval  22949  ustfn  24197  ustval  24198  ustn0  24216  birthdaylem1  26979  nosupno  27733  rgrprc  29528  wksfval  29546  mptctf  32631  measbase  34030  measval  34031  ismeas  34032  isrnmeas  34033  ballotlem2  34322  subfaclefac  35004  satfvsuclem1  35187  dfon2lem2  35608  poimirlem4  37325  poimirlem9  37330  poimirlem26  37347  poimirlem27  37348  poimirlem28  37349  poimirlem32  37353  sdclem2  37443  lineset  39437  lautset  39781  pautsetN  39797  tendoset  40458  eldiophb  42414  rmxyelqirr  42567  hbtlem1  42784  hbtlem7  42786  relopabVD  44577  rabexgf  44623  prprval  47086  upwlksfval  47512
  Copyright terms: Public domain W3C validator