Metamath Proof Explorer


Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep6 ( ∀ 𝑤 ∃* 𝑧 𝜑 → ∃ 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤𝑥 𝜑 ) )

Proof

Step Hyp Ref Expression
1 axrep4v ( ∀ 𝑤𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∃ 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤 ( 𝑤𝑥𝜑 ) ) )
2 df-mo ( ∃* 𝑧 𝜑 ↔ ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) )
3 2 albii ( ∀ 𝑤 ∃* 𝑧 𝜑 ↔ ∀ 𝑤𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) )
4 df-rex ( ∃ 𝑤𝑥 𝜑 ↔ ∃ 𝑤 ( 𝑤𝑥𝜑 ) )
5 4 bibi2i ( ( 𝑧𝑦 ↔ ∃ 𝑤𝑥 𝜑 ) ↔ ( 𝑧𝑦 ↔ ∃ 𝑤 ( 𝑤𝑥𝜑 ) ) )
6 5 albii ( ∀ 𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤𝑥 𝜑 ) ↔ ∀ 𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤 ( 𝑤𝑥𝜑 ) ) )
7 6 exbii ( ∃ 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤𝑥 𝜑 ) ↔ ∃ 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤 ( 𝑤𝑥𝜑 ) ) )
8 1 3 7 3imtr4i ( ∀ 𝑤 ∃* 𝑧 𝜑 → ∃ 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤𝑥 𝜑 ) )