Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2abdv Unicode version

Theorem ss2abdv 3572
 Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
Hypothesis
Ref Expression
ss2abdv.1
Assertion
Ref Expression
ss2abdv
Distinct variable group:   ,

Proof of Theorem ss2abdv
StepHypRef Expression
1 ss2abdv.1 . . 3
21alrimiv 1719 . 2
3 ss2ab 3567 . 2
42, 3sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  A.wal 1393  {cab 2442  C_wss 3475 This theorem is referenced by:  intss  4307  ssopab2  4778  opabbrexOLD  6340  ssoprab2  6353  suppimacnvss  6928  suppimacnv  6929  ressuppss  6938  ss2ixp  7502  fiss  7904  tcss  8196  tcel  8197  infmap2  8619  cfub  8650  cflm  8651  cflecard  8654  cncmet  21761  plyss  22596  ofrn2  27480  sigaclci  28132  subfacp1lem6  28629  ss2mcls  28928  itg2addnclem  30066  sdclem1  30236  istotbnd3  30267  sstotbnd  30271  aomclem4  31003  hbtlem4  31075  hbtlem3  31076  rngunsnply  31122  iocinico  31179 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator