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 2821 | . . . . 5 ⊢ 𝐸 = 𝐸 | |
2 | 1 | rgenw 3150 | . . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸 |
3 | 2 | jctr 527 | . . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
4 | 3 | ralrimivw 3183 | . 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
5 | mpoeq123 7226 | . 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | |
6 | 4, 5 | sylan2 594 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∀wral 3138 ∈ cmpo 7158 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-oprab 7160 df-mpo 7161 |
This theorem is referenced by: dffi3 8895 cantnfres 9140 xpsval 16843 monpropd 17007 grpsubpropd2 18205 lsmvalx 18764 lsmpropd 18803 psrplusgpropd 20404 d1mat2pmat 21347 txval 22172 cnmptk1p 22293 cnmptk2 22294 xpstopnlem1 22417 rrxmval 24008 madjusmdetlem1 31092 pstmval 31135 qqhval2 31223 funcrngcsetc 44318 funcringcsetc 44355 lmod1zr 44597 |
Copyright terms: Public domain | W3C validator |