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

Theorem ss2abi 3659
Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
Hypothesis
Ref Expression
ss2abi.1 (𝜑𝜓)
Assertion
Ref Expression
ss2abi {𝑥𝜑} ⊆ {𝑥𝜓}

Proof of Theorem ss2abi
StepHypRef Expression
1 ss2ab 3655 . 2 ({𝑥𝜑} ⊆ {𝑥𝜓} ↔ ∀𝑥(𝜑𝜓))
2 ss2abi.1 . 2 (𝜑𝜓)
31, 2mpgbir 1723 1 {𝑥𝜑} ⊆ {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  {cab 2607  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-in 3567  df-ss 3574
This theorem is referenced by:  abssi  3662  rabssab  3674  pwpwssunieq  4588  intabs  4795  abssexg  4821  imassrn  5446  fvclss  6465  fabexg  7084  f1oabexg  7087  mapex  7823  tc2  8578  hta  8720  infmap2  9000  cflm  9032  cflim2  9045  hsmex3  9216  domtriomlem  9224  axdc3lem2  9233  brdom7disj  9313  brdom6disj  9314  npex  9768  hashf1lem2  13194  issubc  16435  isghm  17600  symgbasfi  17746  tgval  20699  ustfn  21945  ustval  21946  ustn0  21964  birthdaylem1  24612  rgrprc  26391  wksfval  26409  mptctf  29379  measbase  30083  measval  30084  ismeas  30085  isrnmeas  30086  ballotlem2  30373  subfaclefac  30919  dfon2lem2  31443  nosino  31628  poimirlem4  33084  poimirlem9  33089  poimirlem26  33106  poimirlem27  33107  poimirlem28  33108  poimirlem32  33112  sdclem2  33209  lineset  34543  lautset  34887  pautsetN  34903  tendoset  35566  eldiophb  36839  hbtlem1  37213  hbtlem7  37215  relopabVD  38659  rabexgf  38705  upwlksfval  41034
  Copyright terms: Public domain W3C validator