Theorem ixpeq1

Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006)

	Ref	Expression
Assertion	ixpeq1	⊢ ( 𝐴 = 𝐵 → X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fneq2	⊢ ( 𝐴 = 𝐵 → ( 𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵 ) )
2		raleq	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
3	1 2	anbi12d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
4	3	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } = { 𝑓 ∣ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } )
5		dfixp	⊢ X 𝑥 ∈ 𝐴 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) }
6		dfixp	⊢ X 𝑥 ∈ 𝐵 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) }
7	4 5 6	3eqtr4g	⊢ ( 𝐴 = 𝐵 → X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐶 )