Metamath Proof Explorer

Theorem mh-setind

Description: Principle of set induction setind , written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026)

Ref Expression
Assertion mh-setind 
|- ( A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> ph ) ) -> ph )

Proof

Step Hyp Ref Expression
1 setind 
 |-  ( A. y ( y C_ { x | ph } -> y e. { x | ph } ) -> { x | ph } = _V )
2 ssab 
 |-  ( y C_ { x | ph } <-> A. x ( x e. y -> ph ) )
3 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
4 sb6 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
5 3 4 bitri 
 |-  ( y e. { x | ph } <-> A. x ( x = y -> ph ) )
6 2 5 imbi12i 
 |-  ( ( y C_ { x | ph } -> y e. { x | ph } ) <-> ( A. x ( x e. y -> ph ) -> A. x ( x = y -> ph ) ) )
7 6 albii 
 |-  ( A. y ( y C_ { x | ph } -> y e. { x | ph } ) <-> A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> ph ) ) )
8 abv 
 |-  ( { x | ph } = _V <-> A. x ph )
9 1 7 8 3imtr3i 
 |-  ( A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> ph ) ) -> A. x ph )
10 9 19.21bi 
 |-  ( A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> ph ) ) -> ph )