Theorem abbi 2588

Description: Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Assertion

Ref	Expression
abbi

Proof of Theorem abbi

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hbab1 2445	. . 3
2		hbab1 2445	. . 3
3	1, 2	cleqh 2572	. 2
4		abid 2444	. . . 4
5		abid 2444	. . . 4
6	4, 5	bibi12i 315	. . 3
7	6	albii 1640	. 2
8	3, 7	bitr2i 250	1

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

This theorem is referenced by:  abbii  2591  abbid  2592  nabbi  2790  nabbiOLD  2791  rabbi  3036  sbcbi2  3378  iuneq12df  4354  dfiota2  5557  iotabi  5565  uniabio  5566  iotanul  5571  karden  8334  iuneq12daf  27425  abeq12  30564  elnev  31345  rabeqsn  32919  csbingVD  33684  csbsngVD  33693  csbxpgVD  33694  csbrngVD  33696  csbunigVD  33698  csbfv12gALTVD  33699  bj-cleq  34519

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