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 → χ