Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023)

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

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	⊢ ( ∀ 𝑤 ∃* 𝑧 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )