Metamath Proof Explorer


Theorem setinds2

Description: _E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 setinds2.1 x = y φ ψ
2 setinds2.2 y x ψ φ
3 nfv x ψ
4 3 1 2 setinds2f φ