Metamath Proof Explorer


Theorem setindtrs

Description: Set induction scheme without Infinity. See comments at setindtr . (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Hypotheses setindtrs.a y x ψ φ
setindtrs.b x = y φ ψ
setindtrs.c x = B φ χ
Assertion setindtrs z Tr z B z χ

Proof

Step Hyp Ref Expression
1 setindtrs.a y x ψ φ
2 setindtrs.b x = y φ ψ
3 setindtrs.c x = B φ χ
4 setindtr a a x | φ a x | φ z Tr z B z B x | φ
5 dfss3 a x | φ y a y x | φ
6 nfcv _ x a
7 nfsab1 x y x | φ
8 6 7 nfralw x y a y x | φ
9 nfsab1 x a x | φ
10 8 9 nfim x y a y x | φ a x | φ
11 raleq x = a y x y x | φ y a y x | φ
12 eleq1w x = a x x | φ a x | φ
13 11 12 imbi12d x = a y x y x | φ x x | φ y a y x | φ a x | φ
14 vex y V
15 14 2 elab y x | φ ψ
16 15 ralbii y x y x | φ y x ψ
17 abid x x | φ φ
18 1 16 17 3imtr4i y x y x | φ x x | φ
19 10 13 18 chvarfv y a y x | φ a x | φ
20 5 19 sylbi a x | φ a x | φ
21 4 20 mpg z Tr z B z B x | φ
22 elex B z B V
23 22 adantl Tr z B z B V
24 23 exlimiv z Tr z B z B V
25 3 elabg B V B x | φ χ
26 24 25 syl z Tr z B z B x | φ χ
27 21 26 mpbid z Tr z B z χ