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 abeq2i x V φ
23 2 22 mpbi φ