Theorem ixpv

Description: Infinite Cartesian product of the universal class is the set of functions with a fixed domain. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Assertion	ixpv	⊢ X 𝑥 ∈ 𝐴 V = { 𝑓 ∣ 𝑓 Fn 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		dffn2	⊢ ( 𝑔 Fn 𝐴 ↔ 𝑔 : 𝐴 ⟶ V )
2		vex	⊢ 𝑔 ∈ V
3		fneq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn 𝐴 ↔ 𝑔 Fn 𝐴 ) )
4	2 3	elab	⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 Fn 𝐴 } ↔ 𝑔 Fn 𝐴 )
5	2	elixpconst	⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 V ↔ 𝑔 : 𝐴 ⟶ V )
6	1 4 5	3bitr4ri	⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 V ↔ 𝑔 ∈ { 𝑓 ∣ 𝑓 Fn 𝐴 } )
7	6	eqriv	⊢ X 𝑥 ∈ 𝐴 V = { 𝑓 ∣ 𝑓 Fn 𝐴 }