Metamath Proof Explorer
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 } ) |