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

Metamath Proof Explorer

Theorem axrep6OLD

Description: Obsolete version of axrep6 as of 18-Sep-2025. (Contributed by SN, 18-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-rep ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
2 df-mo ⊢ ( ∃* 𝑧 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
3 19.3v ⊢ ( ∀ 𝑦 𝜑 ↔ 𝜑 )
4 3 imbi1i ⊢ ( ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) )
5 4 albii ⊢ ( ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
6 5 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
7 2 6 bitr4i ⊢ ( ∃* 𝑧 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
8 7 albii ⊢ ( ∀ 𝑤 ∃* 𝑧 𝜑 ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
9 3 rexbii ⊢ ( ∃ 𝑤 ∈ 𝑥 ∀ 𝑦 𝜑 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 )
10 df-rex ⊢ ( ∃ 𝑤 ∈ 𝑥 ∀ 𝑦 𝜑 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) )
11 9 10 bitr3i ⊢ ( ∃ 𝑤 ∈ 𝑥 𝜑 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) )
12 11 bibi2i ⊢ ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
13 12 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
14 13 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
15 1 8 14 3imtr4i ⊢ ( ∀ 𝑤 ∃* 𝑧 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )