mh-setind

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

		Ref	Expression
	Assertion	mh-setind	$⊢ \forall y (\forall x (x \in y \to φ) \to \forall x (x = y \to φ)) \to φ$

Step	Hyp	Ref	Expression
1		setind	$⊢ \forall y (y \subseteq \{x \| φ\} \to y \in \{x \| φ\}) \to \{x \| φ\} = V$
2		ssab	$⊢ y \subseteq \{x \| φ\} \leftrightarrow \forall x (x \in y \to φ)$
3		df-clab	$⊢ y \in \{x \| φ\} \leftrightarrow [y/ x] φ$
4		sb6	$⊢ [y/ x] φ \leftrightarrow \forall x (x = y \to φ)$
5	3 4	bitri	$⊢ y \in \{x \| φ\} \leftrightarrow \forall x (x = y \to φ)$
6	2 5	imbi12i	$⊢ (y \subseteq \{x \| φ\} \to y \in \{x \| φ\}) \leftrightarrow (\forall x (x \in y \to φ) \to \forall x (x = y \to φ))$
7	6	albii	$⊢ \forall y (y \subseteq \{x \| φ\} \to y \in \{x \| φ\}) \leftrightarrow \forall y (\forall x (x \in y \to φ) \to \forall x (x = y \to φ))$
8		abv	$⊢ \{x \| φ\} = V \leftrightarrow \forall x φ$
9	1 7 8	3imtr3i	$⊢ \forall y (\forall x (x \in y \to φ) \to \forall x (x = y \to φ)) \to \forall x φ$
10	9	19.21bi	$⊢ \forall y (\forall x (x \in y \to φ) \to \forall x (x = y \to φ)) \to φ$

Metamath Proof Explorer