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

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
StepHypRef Expression
1 abbi1dv.1 . . . 4
21bicomd 201 . . 3
32abbi2dv 2594 . 2
43eqcomd 2465 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator