Theorem elixpmpt

Description: Membership in an indexed Cartesian product over a set is equivalent to being its exact function graph with components of the indicated types. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypothesis	elixpmpt.a	|- A e. _V
Assertion	elixpmpt	|- ( F e. X_ x e. A B <-> ( F = ( x e. A |-> ( F ` x ) ) /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elixpmpt.a	|- A e. _V
2		elixp2	|- ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
3		3simpc	|- ( ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
4		simpl	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F Fn A )
5		fnex	|- ( ( F Fn A /\ A e. _V ) -> F e. _V )
6	4 1 5	sylancl	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F e. _V )
7		simpr	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> A. x e. A ( F ` x ) e. B )
8	6 4 7	3jca	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
9	3 8	impbii	|- ( ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
10	2 9	bitri	|- ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
11		dffn5	|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
12	10 11	bianbi	|- ( F e. X_ x e. A B <-> ( F = ( x e. A |-> ( F ` x ) ) /\ A. x e. A ( F ` x ) e. B ) )