Metamath Proof Explorer


Theorem setinds2

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

Ref Expression
Hypotheses setinds2.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
setinds2.2 ( ∀ 𝑦𝑥 𝜓𝜑 )
Assertion setinds2 𝜑

Proof

Step Hyp Ref Expression
1 setinds2.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 setinds2.2 ( ∀ 𝑦𝑥 𝜓𝜑 )
3 nfv 𝑥 𝜓
4 3 1 2 setinds2f 𝜑