Theorem ixpsnval

Description: The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018)

	Ref	Expression
Assertion	ixpsnval	⊢ ( 𝑋 ∈ 𝑉 → X 𝑥 ∈ { 𝑋 } 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) } )

Proof

Step	Hyp	Ref	Expression
1		dfixp	⊢ X 𝑥 ∈ { 𝑋 } 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ∀ 𝑥 ∈ { 𝑋 } ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
2		ralsnsg	⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝑋 } ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ [ 𝑋 / 𝑥 ] ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
3		sbcel12	⊢ ( [ 𝑋 / 𝑥 ] ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ⦋ 𝑋 / 𝑥 ⦌ ( 𝑓 ‘ 𝑥 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
4		csbfv2g	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑥 ⦌ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 ) )
5		csbvarg	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑥 ⦌ 𝑥 = 𝑋 )
6	5	fveq2d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑓 ‘ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 ) = ( 𝑓 ‘ 𝑋 ) )
7	4 6	eqtrd	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑥 ⦌ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑋 ) )
8	7	eleq1d	⊢ ( 𝑋 ∈ 𝑉 → ( ⦋ 𝑋 / 𝑥 ⦌ ( 𝑓 ‘ 𝑥 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
9	3 8	bitrid	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
10	2 9	bitrd	⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝑋 } ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
11	10	anbi2d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 Fn { 𝑋 } ∧ ∀ 𝑥 ∈ { 𝑋 } ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
12	11	abbidv	⊢ ( 𝑋 ∈ 𝑉 → { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ∀ 𝑥 ∈ { 𝑋 } ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) } = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) } )
13	1 12	eqtrid	⊢ ( 𝑋 ∈ 𝑉 → X 𝑥 ∈ { 𝑋 } 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) } )