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

Theorem rabbi2dva 3705
 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:   ,   ,   ,

Proof of Theorem rabbi2dva
StepHypRef Expression
1 dfin5 3483 . 2
2 rabbi2dva.1 . . 3
32rabbidva 3100 . 2
41, 3syl5eq 2510 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  {crab 2811  i^icin 3474 This theorem is referenced by:  fndmdif  5991  bitsshft  14125  sylow3lem2  16648  leordtvallem1  19711  leordtvallem2  19712  ordtt1  19880  xkoccn  20120  txcnmpt  20125  xkopt  20156  ordthmeolem  20302  qustgphaus  20621  itg2monolem1  22157  lhop1  22415  efopn  23039  dirith  23714  pjvec  26614  pjocvec  26615  neibastop3  30180  diarnN  36856 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-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-rab 2816  df-in 3482
 Copyright terms: Public domain W3C validator