Theorem ixpeq2 8835

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 8834	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
2		ss2ixp 8834	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → X𝑥 ∈ 𝐴 𝐶 ⊆ X𝑥 ∈ 𝐴 𝐵)
3	1, 2	anim12i 613	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶 ∧ X𝑥 ∈ 𝐴 𝐶 ⊆ X𝑥 ∈ 𝐴 𝐵))
4		eqss 3945	. . . 4 ⊢ (𝐵 = 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
5	4	ralbii 3078	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
6		r19.26 3092	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
7	5, 6	bitri 275	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
8		eqss 3945	. 2 ⊢ (X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶 ↔ (X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶 ∧ X𝑥 ∈ 𝐴 𝐶 ⊆ X𝑥 ∈ 𝐴 𝐵))
9	3, 7, 8	3imtr4i 292	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∀wral 3047   ⊆ wss 3897  Xcixp 8821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-ss 3914  df-ixp 8822

This theorem is referenced by:  ixpeq2dva  8836  ixpint  8849  prdsbas3  17385  pwsbas  17391  ptbasfi  23496  ptunimpt  23510  pttopon  23511  ptcld  23528  ptrescn  23554  ptuncnv  23722  ptunhmeo  23723  ixpeq12i  36243  ptrest  37667  prdstotbnd  37842  ixpeq2d  45113  hoidmv1le  46640