Theorem sn-axrep5v

Description: A condensed form of axrep5 . (Contributed by SN, 21-Sep-2023)

	Ref	Expression
Assertion	sn-axrep5v	⊢ ( ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		axrep6	⊢ ( ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) )
2		19.37v	⊢ ( ∃ 𝑦 ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
3		impexp	⊢ ( ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → ( 𝜑 → 𝑧 = 𝑦 ) ) )
4	3	albii	⊢ ( ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝜑 → 𝑧 = 𝑦 ) ) )
5		19.21v	⊢ ( ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝜑 → 𝑧 = 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
6	4 5	bitri	⊢ ( ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
7	6	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
8		dfmo	⊢ ( ∃* 𝑧 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
9	8	imbi2i	⊢ ( ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ↔ ( 𝑤 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
10	2 7 9	3bitr4i	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
11	10	albii	⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
12		dfmo	⊢ ( ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) )
13	12	albii	⊢ ( ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) )
14		df-ral	⊢ ( ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
15	11 13 14	3bitr4i	⊢ ( ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 )
16		rexanid	⊢ ( ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑤 ∈ 𝑥 𝜑 )
17	16	bibi2i	⊢ ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )
18	17	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )
19	18	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )
20	1 15 19	3imtr3i	⊢ ( ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )