Metamath Proof Explorer


Theorem setinds2f

Description: _E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses setinds2f.1 x ψ
setinds2f.2 x = y φ ψ
setinds2f.3 y x ψ φ
Assertion setinds2f φ

Proof

Step Hyp Ref Expression
1 setinds2f.1 x ψ
2 setinds2f.2 x = y φ ψ
3 setinds2f.3 y x ψ φ
4 sbsbc y x φ [˙y / x]˙ φ
5 1 2 sbiev y x φ ψ
6 4 5 bitr3i [˙y / x]˙ φ ψ
7 6 ralbii y x [˙y / x]˙ φ y x ψ
8 7 3 sylbi y x [˙y / x]˙ φ φ
9 8 setinds φ