| 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 2737 | . . . . 5 ⊢ 𝐸 = 𝐸 | |
| 2 | 1 | rgenw 3065 | . . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸 |
| 3 | 2 | jctr 524 | . . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
| 4 | 3 | ralrimivw 3150 | . 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
| 5 | mpoeq123 7505 | . 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | |
| 6 | 4, 5 | sylan2 593 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∀wral 3061 ∈ cmpo 7433 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-oprab 7435 df-mpo 7436 |
| This theorem is referenced by: dffi3 9471 cantnfres 9717 xpsval 17615 monpropd 17781 grpsubpropd2 19064 lsmvalx 19657 lsmpropd 19695 funcrngcsetc 20640 funcringcsetc 20674 psrplusgpropd 22237 d1mat2pmat 22745 txval 23572 cnmptk1p 23693 cnmptk2 23694 xpstopnlem1 23817 rrxmval 25439 madjusmdetlem1 33826 pstmval 33894 qqhval2 33983 lmod1zr 48410 |
| Copyright terms: Public domain | W3C validator |