This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) } )