![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpoeq12 | Structured version Visualization version GIF version |
Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpoeq12 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2735 | . . . . 5 ⊢ 𝐸 = 𝐸 | |
2 | 1 | rgenw 3063 | . . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸 |
3 | 2 | jctr 524 | . . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
4 | 3 | ralrimivw 3148 | . 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
5 | mpoeq123 7505 | . 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | |
6 | 4, 5 | sylan2 593 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∀wral 3059 ∈ cmpo 7433 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ral 3060 df-oprab 7435 df-mpo 7436 |
This theorem is referenced by: dffi3 9469 cantnfres 9715 xpsval 17617 monpropd 17785 grpsubpropd2 19077 lsmvalx 19672 lsmpropd 19710 funcrngcsetc 20657 funcringcsetc 20691 psrplusgpropd 22253 d1mat2pmat 22761 txval 23588 cnmptk1p 23709 cnmptk2 23710 xpstopnlem1 23833 rrxmval 25453 madjusmdetlem1 33788 pstmval 33856 qqhval2 33945 lmod1zr 48339 |
Copyright terms: Public domain | W3C validator |