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 -> ( ph <-> ps ) )
	setinds2regs.2	|- ( A. y e. x ps -> ph )
Assertion	setinds2regs	|- ph

Proof

Step	Hyp	Ref	Expression
1		setinds2regs.1	|- ( x = y -> ( ph <-> ps ) )
2		setinds2regs.2	|- ( A. y e. x ps -> ph )
3		vex	|- x e. _V
4	1	cbvabv	|- { x | ph } = { y | ps }
5		setindregs	|- ( A. x ( x C_ { y | ps } -> x e. { y | ps } ) -> { y | ps } = _V )
6		ssabral	|- ( x C_ { y | ps } <-> A. y e. x ps )
7	6 2	sylbi	|- ( x C_ { y | ps } -> ph )
8	4	eqabcri	|- ( ph <-> x e. { y | ps } )
9	7 8	sylib	|- ( x C_ { y | ps } -> x e. { y | ps } )
10	5 9	mpg	|- { y | ps } = _V
11	4 10	eqtri	|- { x | ph } = _V
12	11	eqabcri	|- ( ph <-> x e. _V )
13	3 12	mpbir	|- ph