Theorem abbi2dv 2594

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)

Hypothesis

Ref	Expression
abbi2dv.1

Assertion

Ref	Expression
abbi2dv

Distinct variable groups:   ,   ,

Proof of Theorem abbi2dv

Step	Hyp	Ref	Expression
1		abbi2dv.1	. . 3
2	1	alrimiv 1719	. 2
3		abeq2 2581	. 2
4	2, 3	sylibr 212	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442

This theorem is referenced by:  abbi1dv  2595  sbab  2604  iftrue  3947  iffalse  3950  dfopif  4214  iniseg  5373  fncnvima2  6009  isoini  6234  dftpos3  6992  hartogslem1  7988  r1val2  8276  cardval2  8393  dfac3  8523  wrdval  12551  wrdnval  12571  submacs  15996  dfrhm2  17366  lsppr  17739  rspsn  17902  znunithash  18603  tgval3  19464  txrest  20132  xkoptsub  20155  cnextf  20566  cnblcld  21282  shft2rab  21919  sca2rab  21923  grpoinvf  25242  elpjrn  27109  ofrn2  27480  setlikespec  29267  neibastop3  30180  submgmacs  32492  lkrval2  34815  lshpset2N  34844  hdmapoc  37661

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