MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ixpeq2 Structured version   Visualization version   GIF version

Theorem ixpeq2 8905
Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
ixpeq2 (∀𝑥𝐴 𝐵 = 𝐶X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)

Proof of Theorem ixpeq2
StepHypRef Expression
1 ss2ixp 8904 . . 3 (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)
2 ss2ixp 8904 . . 3 (∀𝑥𝐴 𝐶𝐵X𝑥𝐴 𝐶X𝑥𝐴 𝐵)
31, 2anim12i 614 . 2 ((∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵) → (X𝑥𝐴 𝐵X𝑥𝐴 𝐶X𝑥𝐴 𝐶X𝑥𝐴 𝐵))
4 eqss 3998 . . . 4 (𝐵 = 𝐶 ↔ (𝐵𝐶𝐶𝐵))
54ralbii 3094 . . 3 (∀𝑥𝐴 𝐵 = 𝐶 ↔ ∀𝑥𝐴 (𝐵𝐶𝐶𝐵))
6 r19.26 3112 . . 3 (∀𝑥𝐴 (𝐵𝐶𝐶𝐵) ↔ (∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵))
75, 6bitri 275 . 2 (∀𝑥𝐴 𝐵 = 𝐶 ↔ (∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵))
8 eqss 3998 . 2 (X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶 ↔ (X𝑥𝐴 𝐵X𝑥𝐴 𝐶X𝑥𝐴 𝐶X𝑥𝐴 𝐵))
93, 7, 83imtr4i 292 1 (∀𝑥𝐴 𝐵 = 𝐶X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wral 3062  wss 3949  Xcixp 8891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-ixp 8892
This theorem is referenced by:  ixpeq2dva  8906  ixpint  8919  prdsbas3  17427  pwsbas  17433  ptbasfi  23085  ptunimpt  23099  pttopon  23100  ptcld  23117  ptrescn  23143  ptuncnv  23311  ptunhmeo  23312  ptrest  36535  prdstotbnd  36710  ixpeq2d  43803  hoidmv1le  45358
  Copyright terms: Public domain W3C validator