Theorem axrep6g

Description: axrep6 in class notation. It is equivalent to both ax-rep and abrexexg , providing a direct link between the two. (Contributed by SN, 11-Dec-2024)

	Ref	Expression
Assertion	axrep6g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∃* 𝑦 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		rexeq	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ 𝑧 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 𝜓 ) )
2	1	abbidv	⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } )
3	2	eleq1d	⊢ ( 𝑧 = 𝐴 → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) )
4	3	imbi2d	⊢ ( 𝑧 = 𝐴 → ( ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ) ↔ ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) ) )
5		axrep6	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) )
6		abbi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) → { 𝑦 ∣ 𝑦 ∈ 𝑤 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } )
7		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ 𝑤 } = 𝑤
8		vex	⊢ 𝑤 ∈ V
9	7 8	eqeltri	⊢ { 𝑦 ∣ 𝑦 ∈ 𝑤 } ∈ V
10	6 9	eqeltrrdi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V )
11	10	exlimiv	⊢ ( ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V )
12	5 11	syl	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V )
13	4 12	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) )
14	13	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∃* 𝑦 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V )