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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	setinds2regs.2	⊢ ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 )
Assertion	setinds2regs	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		setinds2regs.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		setinds2regs.2	⊢ ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 )
3		vex	⊢ 𝑥 ∈ V
4	1	cbvabv	⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 }
5		setindregs	⊢ ( ∀ 𝑥 ( 𝑥 ⊆ { 𝑦 ∣ 𝜓 } → 𝑥 ∈ { 𝑦 ∣ 𝜓 } ) → { 𝑦 ∣ 𝜓 } = V )
6		ssabral	⊢ ( 𝑥 ⊆ { 𝑦 ∣ 𝜓 } ↔ ∀ 𝑦 ∈ 𝑥 𝜓 )
7	6 2	sylbi	⊢ ( 𝑥 ⊆ { 𝑦 ∣ 𝜓 } → 𝜑 )
8	4	eqabcri	⊢ ( 𝜑 ↔ 𝑥 ∈ { 𝑦 ∣ 𝜓 } )
9	7 8	sylib	⊢ ( 𝑥 ⊆ { 𝑦 ∣ 𝜓 } → 𝑥 ∈ { 𝑦 ∣ 𝜓 } )
10	5 9	mpg	⊢ { 𝑦 ∣ 𝜓 } = V
11	4 10	eqtri	⊢ { 𝑥 ∣ 𝜑 } = V
12	11	eqabcri	⊢ ( 𝜑 ↔ 𝑥 ∈ V )
13	3 12	mpbir	⊢ 𝜑