This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )