Theorem mh-setind

Description: Principle of set induction setind , written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026)

	Ref	Expression
Assertion	mh-setind	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		setind	⊢ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) → { 𝑥 ∣ 𝜑 } = V )
2		ssab	⊢ ( 𝑦 ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) )
3		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
4		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
5	3 4	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
6	2 5	imbi12i	⊢ ( ( 𝑦 ⊆ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
7	6	albii	⊢ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
8		abv	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 )
9	1 7 8	3imtr3i	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ∀ 𝑥 𝜑 )
10	9	19.21bi	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → 𝜑 )