This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abbii

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

Ref Expression
Hypothesis abbii.1 
|- ( ph <-> ps )
Assertion abbii 
|- { x | ph } = { x | ps }

Proof

Step Hyp Ref Expression
1 abbii.1 
 |-  ( ph <-> ps )
2 abbi 
 |-  ( A. x ( ph <-> ps ) -> { x | ph } = { x | ps } )
3 2 1 mpg 
 |-  { x | ph } = { x | ps }