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

Theorem ixpeq1 8128
Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
ixpeq1 (𝐴 = 𝐵X𝑥𝐴 𝐶 = X𝑥𝐵 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem ixpeq1
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 fneq2 6160 . . . 4 (𝐴 = 𝐵 → (𝑓 Fn 𝐴𝑓 Fn 𝐵))
2 raleq 3286 . . . 4 (𝐴 = 𝐵 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶 ↔ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶))
31, 2anbi12d 624 . . 3 (𝐴 = 𝐵 → ((𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶) ↔ (𝑓 Fn 𝐵 ∧ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶)))
43abbidv 2884 . 2 (𝐴 = 𝐵 → {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)} = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶)})
5 dfixp 8119 . 2 X𝑥𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)}
6 dfixp 8119 . 2 X𝑥𝐵 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶)}
74, 5, 63eqtr4g 2824 1 (𝐴 = 𝐵X𝑥𝐴 𝐶 = X𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  {cab 2751  wral 3055   Fn wfn 6065  cfv 6070  Xcixp 8117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-fn 6073  df-ixp 8118
This theorem is referenced by:  ixpeq1d  8129  finixpnum  33839  ioorrnopn  41186  ioorrnopnxr  41188  ovnval  41419  hoicvr  41426  hoidmv1le  41472  hoidmvle  41478  ovnhoi  41481  hspval  41487  ovnlecvr2  41488  hoiqssbl  41503  vonhoire  41550  iunhoiioo  41554  vonioo  41560  vonicc  41563
  Copyright terms: Public domain W3C validator