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

Step	Hyp	Ref	Expression
1		dfin5 3483	. 2
2		rabbi2dva.1	. . 3
3	2	rabbidva 3100	. 2
4	1, 3	syl5eq 2510	1

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