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

Metamath Proof Explorer

Theorem axrep4OLD

Description: Obsolete version of axrep4 as of 18-Sep-2025. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis axrep4OLD.1 ⊢ Ⅎ 𝑧 𝜑
Assertion axrep4OLD ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 axrep4OLD.1 ⊢ Ⅎ 𝑧 𝜑
2 axrep3 ⊢ ∃ 𝑥 ( ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
3 2 19.35i ⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
4 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ 𝑥
5 nfv ⊢ Ⅎ 𝑧 𝑥 ∈ 𝑤
6 nfa1 ⊢ Ⅎ 𝑧 ∀ 𝑧 𝜑
7 5 6 nfan ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 )
8 7 nfex ⊢ Ⅎ 𝑧 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 )
9 4 8 nfbi ⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) )
10 9 nfal ⊢ Ⅎ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) )
11 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝑧
12 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 )
13 11 12 nfbi ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
14 13 nfal ⊢ Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
15 elequ2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 ) )
16 1 19.3 ⊢ ( ∀ 𝑧 𝜑 ↔ 𝜑 )
17 16 anbi2i ⊢ ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
18 17 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
19 18 a1i ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
20 15 19 bibi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) )
21 20 albidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) )
22 10 14 21 cbvexv1 ⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
23 3 22 sylib ⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )