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 )