Theorem ixpeq2 8940

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

Assertion

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

Proof of Theorem ixpeq2

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∀wral 3077   ⊆ wss 3914  Xcixp 8926

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-ss 3915  df-ixp 8927

This theorem is used by:  ixpeq2dva  8941  ixpint  8954  prdsbas3  17653  pwsbas  17659  ptbasfi  23901  ptunimpt  23915  pttopon  23916  ptcld  23933  ptrescn  23959  ptuncnv  24127  ptunhmeo  24128  ixpeq12i  36991  ptrest  38539  prdstotbnd  38730  ixpeq2d  46086  hoidmv1le  47605