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 𝑥 𝜓
setinds2f.2 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
setinds2f.3 ( ∀ 𝑦𝑥 𝜓𝜑 )
Assertion setinds2f 𝜑

Proof

Step Hyp Ref Expression
1 setinds2f.1 𝑥 𝜓
2 setinds2f.2 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
3 setinds2f.3 ( ∀ 𝑦𝑥 𝜓𝜑 )
4 sbsbc ( [ 𝑦 / 𝑥 ] 𝜑[ 𝑦 / 𝑥 ] 𝜑 )
5 1 2 sbiev ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
6 4 5 bitr3i ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
7 6 ralbii ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦𝑥 𝜓 )
8 7 3 sylbi ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 )
9 8 setinds 𝜑