Theorem abbi 2579

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	|- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )

Proof of Theorem abbi

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hbab1 2438	. . 3 |- ( y e. { x | ph } -> A. x y e. { x | ph } )
2		hbab1 2438	. . 3 |- ( y e. { x | ps } -> A. x y e. { x | ps } )
3	1, 2	cleqh 2563	. 2 |- ( { x | ph } = { x | ps } <-> A. x ( x e. { x | ph } <-> x e. { x | ps } ) )
4		abid 2437	. . . 4 |- ( x e. { x | ph } <-> ph )
5		abid 2437	. . . 4 |- ( x e. { x | ps } <-> ps )
6	4, 5	bibi12i 315	. . 3 |- ( ( x e. { x | ph } <-> x e. { x | ps } ) <-> ( ph <-> ps ) )
7	6	albii 1611	. 2 |- ( A. x ( x e. { x | ph } <-> x e. { x | ps } ) <-> A. x ( ph <-> ps ) )
8	3, 7	bitr2i 250	1 |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )

Syntax hints:   <-> wb 184   A.wal 1368   = wceq 1370   e. wcel 1757   {cab 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445

This theorem is referenced by:  abbii  2582  abbid  2583  nabbi  2778  nabbiOLD  2779  rabbi  2981  sbcbi2  3321  iuneq12df  4278  dfiota2  5466  iotabi  5474  uniabio  5475  iotanul  5480  karden  8189  iuneq12daf  26028  abeq12  29092  elnev  29816  rabeqsn  30841  csbingVD  31902  csbsngVD  31911  csbxpgVD  31912  csbrngVD  31914  csbunigVD  31916  csbfv12gALTVD  31917  bj-cleq  32736