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

Theorem ss2abi 4024
Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2109, ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.)
Hypothesis
Ref Expression
ss2abi.1 (𝜑𝜓)
Assertion
Ref Expression
ss2abi {𝑥𝜑} ⊆ {𝑥𝜓}

Proof of Theorem ss2abi
StepHypRef Expression
1 tru 1546 . 2
2 ss2abi.1 . . . 4 (𝜑𝜓)
32a1i 11 . . 3 (⊤ → (𝜑𝜓))
43ss2abdv 4021 . 2 (⊤ → {𝑥𝜑} ⊆ {𝑥𝜓})
51, 4ax-mp 5 1 {𝑥𝜑} ⊆ {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1543  {cab 2710  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-in 3918  df-ss 3928
This theorem is referenced by:  abssi  4028  rabssab  4044  abanssl  4262  abanssr  4263  pwpwssunieq  5065  intabs  5300  abssexg  5338  imassrn  6025  fvclss  7190  fabexg  7872  f1oabexg  7874  mapex  8774  f1osetex  8800  fsetexb  8805  tc2  9683  hta  9838  infmap2  10159  cflm  10191  cflim2  10204  hsmex3  10375  domtriomlem  10383  axdc3lem2  10392  brdom7disj  10472  brdom6disj  10473  npex  10927  hashf1lem2  14361  issubc  17726  isghm  19013  permsetexOLD  19156  symgbas  19157  symgbasfi  19165  tgval  22321  ustfn  23569  ustval  23570  ustn0  23588  birthdaylem1  26317  nosupno  27067  rgrprc  28581  wksfval  28599  mptctf  31681  measbase  32853  measval  32854  ismeas  32855  isrnmeas  32856  ballotlem2  33145  subfaclefac  33827  satfvsuclem1  34010  dfon2lem2  34415  poimirlem4  36128  poimirlem9  36133  poimirlem26  36150  poimirlem27  36151  poimirlem28  36152  poimirlem32  36156  sdclem2  36247  lineset  38247  lautset  38591  pautsetN  38607  tendoset  39268  eldiophb  41123  rmxyelqirr  41276  hbtlem1  41493  hbtlem7  41495  relopabVD  43271  rabexgf  43317  prprval  45792  upwlksfval  46123
  Copyright terms: Public domain W3C validator