Theorem ixp0x

Description: An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007)

	Ref	Expression
Assertion	ixp0x	⊢ X 𝑥 ∈ ∅ 𝐴 = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		dfixp	⊢ X 𝑥 ∈ ∅ 𝐴 = { 𝑓 ∣ ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) }
2		velsn	⊢ ( 𝑓 ∈ { ∅ } ↔ 𝑓 = ∅ )
3		fn0	⊢ ( 𝑓 Fn ∅ ↔ 𝑓 = ∅ )
4		ral0	⊢ ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) ∈ 𝐴
5	4	biantru	⊢ ( 𝑓 Fn ∅ ↔ ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) )
6	2 3 5	3bitr2i	⊢ ( 𝑓 ∈ { ∅ } ↔ ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) )
7	6	abbi2i	⊢ { ∅ } = { 𝑓 ∣ ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) }
8	1 7	eqtr4i	⊢ X 𝑥 ∈ ∅ 𝐴 = { ∅ }