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

Theorem ixpeq2 8952
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 8951 . . 3 (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)
2 ss2ixp 8951 . . 3 (∀𝑥𝐴 𝐶𝐵X𝑥𝐴 𝐶X𝑥𝐴 𝐵)
31, 2anim12i 613 . 2 ((∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵) → (X𝑥𝐴 𝐵X𝑥𝐴 𝐶X𝑥𝐴 𝐶X𝑥𝐴 𝐵))
4 eqss 3998 . . . 4 (𝐵 = 𝐶 ↔ (𝐵𝐶𝐶𝐵))
54ralbii 3092 . . 3 (∀𝑥𝐴 𝐵 = 𝐶 ↔ ∀𝑥𝐴 (𝐵𝐶𝐶𝐵))
6 r19.26 3110 . . 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 395   = wceq 1539  wral 3060  wss 3950  Xcixp 8938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-ss 3967  df-ixp 8939
This theorem is referenced by:  ixpeq2dva  8953  ixpint  8966  prdsbas3  17527  pwsbas  17533  ptbasfi  23590  ptunimpt  23604  pttopon  23605  ptcld  23622  ptrescn  23648  ptuncnv  23816  ptunhmeo  23817  ixpeq12i  36203  ptrest  37627  prdstotbnd  37802  ixpeq2d  45078  hoidmv1le  46614
  Copyright terms: Public domain W3C validator