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

Metamath Proof Explorer

Theorem abbi1sn

Description: Originally part of uniabio . Convert a theorem about df-iota to one about dfiota2 , without ax-10 , ax-11 , ax-12 . Although, eu6 uses ax-10 and ax-12 . (Contributed by SN, 23-Nov-2024)

Ref Expression
Assertion abbi1sn 
|- ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )

Proof

Step Hyp Ref Expression
1 abbi 
 |-  ( A. x ( ph <-> x = y ) -> { x | ph } = { x | x = y } )
2 df-sn 
 |-  { y } = { x | x = y }
3 1 2 eqtr4di 
 |-  ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )