![]() |
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 6642 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵)) | |
2 | raleq 3323 | . . . 4 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)) | |
3 | 1, 2 | anbi12d 632 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶) ↔ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶))) |
4 | 3 | abbidv 2802 | . 2 ⊢ (𝐴 = 𝐵 → {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)}) |
5 | dfixp 8893 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} | |
6 | dfixp 8893 | . 2 ⊢ X𝑥 ∈ 𝐵 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)} | |
7 | 4, 5, 6 | 3eqtr4g 2798 | 1 ⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 {cab 2710 ∀wral 3062 Fn wfn 6539 ‘cfv 6544 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-rex 3072 df-fn 6547 df-ixp 8892 |
This theorem is referenced by: ixpeq1d 8903 finixpnum 36521 ioorrnopn 45069 ioorrnopnxr 45071 ovnval 45305 hoicvr 45312 hoidmv1le 45358 hoidmvle 45364 ovnhoi 45367 hspval 45373 ovnlecvr2 45374 hoiqssbl 45389 vonhoire 45436 iunhoiioo 45440 vonioo 45446 vonicc 45449 |
Copyright terms: Public domain | W3C validator |