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 ⊢∃zTr⁡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 ⊢∀aa⊆x|φ→a∈x|φ→∃zTr⁡z∧B∈z→B∈x|φ
5 dfss3 ⊢a⊆x|φ↔∀y∈ay∈x|φ
6 nfcv ⊢Ⅎ_xa
7 nfsab1 ⊢Ⅎxy∈x|φ
8 6 7 nfralw ⊢Ⅎx∀y∈ay∈x|φ
9 nfsab1 ⊢Ⅎxa∈x|φ
10 8 9 nfim ⊢Ⅎx∀y∈ay∈x|φ→a∈x|φ
11 raleq ⊢x=a→∀y∈xy∈x|φ↔∀y∈ay∈x|φ
12 eleq1w ⊢x=a→x∈x|φ↔a∈x|φ
13 11 12 imbi12d ⊢x=a→∀y∈xy∈x|φ→x∈x|φ↔∀y∈ay∈x|φ→a∈x|φ
14 vex ⊢y∈V
15 14 2 elab ⊢y∈x|φ↔ψ
16 15 ralbii ⊢∀y∈xy∈x|φ↔∀y∈xψ
17 abid ⊢x∈x|φ↔φ
18 1 16 17 3imtr4i ⊢∀y∈xy∈x|φ→x∈x|φ
19 10 13 18 chvarfv ⊢∀y∈ay∈x|φ→a∈x|φ
20 5 19 sylbi ⊢a⊆x|φ→a∈x|φ
21 4 20 mpg ⊢∃zTr⁡z∧B∈z→B∈x|φ
22 elex ⊢B∈z→B∈V
23 22 adantl ⊢Tr⁡z∧B∈z→B∈V
24 23 exlimiv ⊢∃zTr⁡z∧B∈z→B∈V
25 3 elabg ⊢B∈V→B∈x|φ↔χ
26 24 25 syl ⊢∃zTr⁡z∧B∈z→B∈x|φ↔χ
27 21 26 mpbid ⊢∃zTr⁡z∧B∈z→χ