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