![]() |
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 2730 | . . . . 5 ⊢ 𝐸 = 𝐸 | |
2 | 1 | rgenw 3063 | . . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸 |
3 | 2 | jctr 523 | . . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
4 | 3 | ralrimivw 3148 | . 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) |
5 | mpoeq123 7483 | . 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | |
6 | 4, 5 | sylan2 591 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1539 ∀wral 3059 ∈ cmpo 7413 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ral 3060 df-oprab 7415 df-mpo 7416 |
This theorem is referenced by: dffi3 9428 cantnfres 9674 xpsval 17520 monpropd 17688 grpsubpropd2 18965 lsmvalx 19548 lsmpropd 19586 psrplusgpropd 21978 d1mat2pmat 22461 txval 23288 cnmptk1p 23409 cnmptk2 23410 xpstopnlem1 23533 rrxmval 25153 madjusmdetlem1 33105 pstmval 33173 qqhval2 33260 funcrngcsetc 46984 funcringcsetc 47021 lmod1zr 47261 |
Copyright terms: Public domain | W3C validator |