Theorem abbi1dv 2595

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypothesis

Ref	Expression
abbi1dv.1

Assertion

Ref	Expression
abbi1dv

Distinct variable groups:   ,   ,

Proof of Theorem abbi1dv

Step	Hyp	Ref	Expression
1		abbi1dv.1	. . . 4
2	1	bicomd 201	. . 3
3	2	abbi2dv 2594	. 2
4	3	eqcomd 2465	1

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

This theorem is referenced by:  abidnf  3268  csbtt  3445  csbie2g  3465  abvor0  3803  csbvarg  3848  iinxsng  4407  enfin2i  8722  fin1a2lem11  8811  hashf1  12506  shftuz  12902  psrbaglefi  18023  psrbaglefiOLD  18024  vmappw  23390  predep  29272  hdmap1fval  37524  hdmapfval  37557  hgmapfval  37616

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