Theorem ixpeq2 8849

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 8848	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
2		ss2ixp 8848	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → X𝑥 ∈ 𝐴 𝐶 ⊆ X𝑥 ∈ 𝐴 𝐵)
3	1, 2	anim12i 619	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶 ∧ X𝑥 ∈ 𝐴 𝐶 ⊆ X𝑥 ∈ 𝐴 𝐵))
4		eqss 3930	. . . 4 ⊢ (𝐵 = 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
5	4	ralbii 3085	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
6		r19.26 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
7	5, 6	bitri 276	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
8		eqss 3930	. 2 ⊢ (X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶 ↔ (X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶 ∧ X𝑥 ∈ 𝐴 𝐶 ⊆ X𝑥 ∈ 𝐴 𝐵))
9	3, 7, 8	3imtr4i 293	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ∀wral 3053   ⊆ wss 3883  Xcixp 8835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-ss 3900  df-ixp 8836

This theorem is referenced by:  ixpeq2dva  8850  ixpint  8863  prdsbas3  17435  pwsbas  17441  ptbasfi  23564  ptunimpt  23578  pttopon  23579  ptcld  23596  ptrescn  23622  ptuncnv  23790  ptunhmeo  23791  ixpeq12i  36429  ptrest  37986  prdstotbnd  38161  ixpeq2d  45516  hoidmv1le  47037