Theorem abbi 2527

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 2384	. . 3 |- ( y e. { x | ph } -> A. x y e. { x | ph } )
2		hbab1 2384	. . 3 |- ( y e. { x | ps } -> A. x y e. { x | ps } )
3	1, 2	cleqh 2511	. 2 |- ( { x | ph } = { x | ps } <-> A. x ( x e. { x | ph } <-> x e. { x | ps } ) )
4		abid 2383	. . . 4 |- ( x e. { x | ph } <-> ph )
5		abid 2383	. . . 4 |- ( x e. { x | ps } <-> ps )
6	4, 5	bibi12i 313	. . 3 |- ( ( x e. { x | ph } <-> x e. { x | ps } ) <-> ( ph <-> ps ) )
7	6	albii 1655	. 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 1397   = wceq 1399   e. wcel 1836   {cab 2381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391

This theorem is referenced by:  abbii  2530  abbid  2531  nabbi  2729  nabbiOLD  2730  rabbi  2978  sbcbi2  3318  iuneq12df  4284  dfiota2  5478  iotabi  5486  uniabio  5487  iotanul  5492  karden  8248  iuneq12daf  27583  abeq12  30770  elnev  31553  rabeqsn  33158  csbingVD  34070  csbsngVD  34079  csbxpgVD  34080  csbrngVD  34082  csbunigVD  34084  csbfv12gALTVD  34085  bj-cleq  34906