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

Theorem rabbi2dva 3676
 Description: Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
Hypothesis
Ref Expression
rabbi2dva.1
Assertion
Ref Expression
rabbi2dva
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem rabbi2dva
StepHypRef Expression
1 dfin5 3450 . 2
2 rabbi2dva.1 . . 3
32rabbidva 3078 . 2
41, 3syl5eq 2482 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1870  crab 2786   cin 3441 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2787  df-rab 2791  df-in 3449 This theorem is referenced by:  fndmdif  6001  bitsshft  14423  sylow3lem2  17215  leordtvallem1  20157  leordtvallem2  20158  ordtt1  20326  xkoccn  20565  txcnmpt  20570  xkopt  20601  ordthmeolem  20747  qustgphaus  21068  itg2monolem1  22585  lhop1  22843  efopn  23468  dirith  24230  pjvec  27184  pjocvec  27185  neibastop3  30803  diarnN  34406
 Copyright terms: Public domain W3C validator