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

Metamath Proof Explorer

Theorem setinds

Description: Principle of set induction (or _E -induction). If a property passes from all elements of x to x itself, then it holds for all x . (Contributed by Scott Fenton, 10-Mar-2011)

Ref Expression
Hypothesis setinds.1 ⊢ ∀ y ∈ x [˙y / x]˙ φ → φ
Assertion setinds ⊢ φ

Proof

Step Hyp Ref Expression
1 setinds.1 ⊢ ∀ y ∈ x [˙y / x]˙ φ → φ
2 vex ⊢ x ∈ V
3 setind ⊢ ∀ z z ⊆ x | φ → z ∈ x | φ → x | φ = V
4 dfss3 ⊢ z ⊆ x | φ ↔ ∀ y ∈ z y ∈ x | φ
5 df-sbc ⊢ [˙y / x]˙ φ ↔ y ∈ x | φ
6 5 ralbii ⊢ ∀ y ∈ z [˙y / x]˙ φ ↔ ∀ y ∈ z y ∈ x | φ
7 nfcv ⊢ Ⅎ _ x z
8 nfsbc1v ⊢ Ⅎ x [˙y / x]˙ φ
9 7 8 nfralw ⊢ Ⅎ x ∀ y ∈ z [˙y / x]˙ φ
10 nfsbc1v ⊢ Ⅎ x [˙z / x]˙ φ
11 9 10 nfim ⊢ Ⅎ x ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
12 raleq ⊢ x = z → ∀ y ∈ x [˙y / x]˙ φ ↔ ∀ y ∈ z [˙y / x]˙ φ
13 sbceq1a ⊢ x = z → φ ↔ [˙z / x]˙ φ
14 12 13 imbi12d ⊢ x = z → ∀ y ∈ x [˙y / x]˙ φ → φ ↔ ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
15 11 14 1 chvarfv ⊢ ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
16 6 15 sylbir ⊢ ∀ y ∈ z y ∈ x | φ → [˙z / x]˙ φ
17 4 16 sylbi ⊢ z ⊆ x | φ → [˙z / x]˙ φ
18 df-sbc ⊢ [˙z / x]˙ φ ↔ z ∈ x | φ
19 17 18 sylib ⊢ z ⊆ x | φ → z ∈ x | φ
20 3 19 mpg ⊢ x | φ = V
21 20 eqcomi ⊢ V = x | φ
22 21 eqabri ⊢ x ∈ V ↔ φ
23 2 22 mpbi ⊢ φ