Theorem setinds2regs

Description: Principle of set induction (or _E -induction). If a property passes from all elements of x to x itself, then it holds for all x . (Contributed by BTernaryTau, 31-Dec-2025)

	Ref	Expression
Hypotheses	setinds2regs.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	setinds2regs.2	$$⊢\forall y\in x\psi \to \phi$$
Assertion	setinds2regs	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		setinds2regs.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		setinds2regs.2	$$⊢\forall y\in x\psi \to \phi$$
3		vex	$$⊢x\in \mathrm{V}$$
4	1	cbvabv	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$
5		setindregs	$$⊢\forall x\left(x\subseteq \left\{y|\psi \right\}\to x\in \left\{y|\psi \right\}\right)\to \left\{y|\psi \right\}=\mathrm{V}$$
6		ssabral	$$⊢x\subseteq \left\{y|\psi \right\}\leftrightarrow \forall y\in x\psi$$
7	6 2	sylbi	$$⊢x\subseteq \left\{y|\psi \right\}\to \phi$$
8	4	eqabcri	$$⊢\phi \leftrightarrow x\in \left\{y|\psi \right\}$$
9	7 8	sylib	$$⊢x\subseteq \left\{y|\psi \right\}\to x\in \left\{y|\psi \right\}$$
10	5 9	mpg	$$⊢\left\{y|\psi \right\}=\mathrm{V}$$
11	4 10	eqtri	$$⊢\left\{x|\phi \right\}=\mathrm{V}$$
12	11	eqabcri	$$⊢\phi \leftrightarrow x\in \mathrm{V}$$
13	3 12	mpbir	$$⊢\phi$$