This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝜑