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

Theorem ixpeq1 8471
 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 6444 . . . 4 (𝐴 = 𝐵 → (𝑓 Fn 𝐴𝑓 Fn 𝐵))
2 raleq 3405 . . . 4 (𝐴 = 𝐵 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶 ↔ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶))
31, 2anbi12d 632 . . 3 (𝐴 = 𝐵 → ((𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶) ↔ (𝑓 Fn 𝐵 ∧ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶)))
43abbidv 2885 . 2 (𝐴 = 𝐵 → {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)} = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶)})
5 dfixp 8462 . 2 X𝑥𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)}
6 dfixp 8462 . 2 X𝑥𝐵 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥𝐵 (𝑓𝑥) ∈ 𝐶)}
74, 5, 63eqtr4g 2881 1 (𝐴 = 𝐵X𝑥𝐴 𝐶 = X𝑥𝐵 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {cab 2799  ∀wral 3138   Fn wfn 6349  ‘cfv 6354  Xcixp 8460 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-fn 6357  df-ixp 8461 This theorem is referenced by:  ixpeq1d  8472  finixpnum  34876  ioorrnopn  42591  ioorrnopnxr  42593  ovnval  42824  hoicvr  42831  hoidmv1le  42877  hoidmvle  42883  ovnhoi  42886  hspval  42892  ovnlecvr2  42893  hoiqssbl  42908  vonhoire  42955  iunhoiioo  42959  vonioo  42965  vonicc  42968
 Copyright terms: Public domain W3C validator