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 2733 | . . . . 5 ⊢ 𝐸 = 𝐸 | |
2 | 1 | rgenw 3063 | . . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸 |
3 | 2 | jctr 524 | . . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
4 | 3 | ralrimivw 3141 | . 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
5 | mpoeq123 7367 | . 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | |
6 | 4, 5 | sylan2 592 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∀wral 3059 ∈ cmpo 7297 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-tru 1540 df-ex 1778 df-nf 1782 df-sb 2063 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ral 3060 df-oprab 7299 df-mpo 7300 |
This theorem is referenced by: dffi3 9218 cantnfres 9463 xpsval 17309 monpropd 17477 grpsubpropd2 18709 lsmvalx 19272 lsmpropd 19311 psrplusgpropd 21435 d1mat2pmat 21916 txval 22743 cnmptk1p 22864 cnmptk2 22865 xpstopnlem1 22988 rrxmval 24597 madjusmdetlem1 31805 pstmval 31873 qqhval2 31960 funcrngcsetc 45596 funcringcsetc 45633 lmod1zr 45874 |
Copyright terms: Public domain | W3C validator |