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

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