Theorem ixpeq2

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

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

Proof

Step	Hyp	Ref	Expression
1		ss2ixp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X 𝑥 ∈ 𝐴 𝐵 ⊆ X 𝑥 ∈ 𝐴 𝐶 )
2		ss2ixp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → X 𝑥 ∈ 𝐴 𝐶 ⊆ X 𝑥 ∈ 𝐴 𝐵 )
3	1 2	anim12i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ) → ( X 𝑥 ∈ 𝐴 𝐵 ⊆ X 𝑥 ∈ 𝐴 𝐶 ∧ X 𝑥 ∈ 𝐴 𝐶 ⊆ X 𝑥 ∈ 𝐴 𝐵 ) )
4		eqss	⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) )
5	4	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) )
6		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ) )
7	5 6	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ) )
8		eqss	⊢ ( X 𝑥 ∈ 𝐴 𝐵 = X 𝑥 ∈ 𝐴 𝐶 ↔ ( X 𝑥 ∈ 𝐴 𝐵 ⊆ X 𝑥 ∈ 𝐴 𝐶 ∧ X 𝑥 ∈ 𝐴 𝐶 ⊆ X 𝑥 ∈ 𝐴 𝐵 ) )
9	3 7 8	3imtr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → X 𝑥 ∈ 𝐴 𝐵 = X 𝑥 ∈ 𝐴 𝐶 )