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 ⊢ A ∈ V ∧ ∀ x ∃* y ψ → y | ∃ x ∈ A ψ ∈ V

Proof

Step Hyp Ref Expression
1 rexeq ⊢ z = A → ∃ x ∈ z ψ ↔ ∃ x ∈ A ψ
2 1 abbidv ⊢ z = A → y | ∃ x ∈ z ψ = y | ∃ x ∈ A ψ
3 2 eleq1d ⊢ z = A → y | ∃ x ∈ z ψ ∈ V ↔ y | ∃ x ∈ A ψ ∈ V
4 3 imbi2d ⊢ z = A → ∀ x ∃* y ψ → y | ∃ x ∈ z ψ ∈ V ↔ ∀ x ∃* y ψ → y | ∃ x ∈ A ψ ∈ V
5 axrep6 ⊢ ∀ x ∃* y ψ → ∃ w ∀ y y ∈ w ↔ ∃ x ∈ z ψ
6 abbi ⊢ ∀ y y ∈ w ↔ ∃ x ∈ z ψ → y | y ∈ w = y | ∃ x ∈ z ψ
7 abid2 ⊢ y | y ∈ w = w
8 vex ⊢ w ∈ V
9 7 8 eqeltri ⊢ y | y ∈ w ∈ V
10 6 9 eqeltrrdi ⊢ ∀ y y ∈ w ↔ ∃ x ∈ z ψ → y | ∃ x ∈ z ψ ∈ V
11 10 exlimiv ⊢ ∃ w ∀ y y ∈ w ↔ ∃ x ∈ z ψ → y | ∃ x ∈ z ψ ∈ V
12 5 11 syl ⊢ ∀ x ∃* y ψ → y | ∃ x ∈ z ψ ∈ V
13 4 12 vtoclg ⊢ A ∈ V → ∀ x ∃* y ψ → y | ∃ x ∈ A ψ ∈ V
14 13 imp ⊢ A ∈ V ∧ ∀ x ∃* y ψ → y | ∃ x ∈ A ψ ∈ V