|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ixpeq1 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) | 
| Ref | Expression | 
|---|---|
| ixpeq1 | ⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | fneq2 6659 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵)) | |
| 2 | raleq 3322 | . . . 4 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)) | |
| 3 | 1, 2 | anbi12d 632 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶) ↔ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶))) | 
| 4 | 3 | abbidv 2807 | . 2 ⊢ (𝐴 = 𝐵 → {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)}) | 
| 5 | dfixp 8940 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} | |
| 6 | dfixp 8940 | . 2 ⊢ X𝑥 ∈ 𝐵 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)} | |
| 7 | 4, 5, 6 | 3eqtr4g 2801 | 1 ⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 {cab 2713 ∀wral 3060 Fn wfn 6555 ‘cfv 6560 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-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 df-fn 6563 df-ixp 8939 | 
| This theorem is referenced by: ixpeq1d 8950 finixpnum 37613 ioorrnopn 46325 ioorrnopnxr 46327 ovnval 46561 hoicvr 46568 hoidmv1le 46614 hoidmvle 46620 ovnhoi 46623 hspval 46629 ovnlecvr2 46630 hoiqssbl 46645 vonhoire 46692 iunhoiioo 46696 vonioo 46702 vonicc 46705 | 
| Copyright terms: Public domain | W3C validator |