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_ x e. A _V = { f | f Fn A }

Proof

Step	Hyp	Ref	Expression
1		dffn2	|- ( g Fn A <-> g : A --> _V )
2		vex	|- g e. _V
3		fneq1	|- ( f = g -> ( f Fn A <-> g Fn A ) )
4	2 3	elab	|- ( g e. { f | f Fn A } <-> g Fn A )
5	2	elixpconst	|- ( g e. X_ x e. A _V <-> g : A --> _V )
6	1 4 5	3bitr4ri	|- ( g e. X_ x e. A _V <-> g e. { f | f Fn A } )
7	6	eqriv	|- X_ x e. A _V = { f | f Fn A }