![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpteq12dva | Structured version Visualization version GIF version |
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Ref | Expression |
---|---|
mpteq12dv.1 | ⊢ (𝜑 → 𝐴 = 𝐶) |
mpteq12dva.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
mpteq12dva | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq12dv.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐶) | |
2 | 1 | alrimiv 1887 | . 2 ⊢ (𝜑 → ∀𝑥 𝐴 = 𝐶) |
3 | mpteq12dva.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) | |
4 | 3 | ralrimiva 3127 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) |
5 | mpteq12f 5007 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | |
6 | 2, 4, 5 | syl2anc 576 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∀wal 1506 = wceq 1508 ∈ wcel 2051 ∀wral 3083 ↦ cmpt 5005 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-12 2107 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-ral 3088 df-opab 4989 df-mpt 5006 |
This theorem is referenced by: mpteq12dv 5009 pfxmpt 13859 reps 13988 repswccat 14004 cidpropd 16851 monpropd 16878 fucpropd 17118 curfpropd 17354 hofpropd 17388 yonffthlem 17403 ofco2 20780 pmatcollpw3fi1lem1 21114 rrxnm 23713 ushgredgedg 26730 ushgredgedgloop 26732 cshw1s2 30394 cycpm2tr 30481 sgnsv 30501 extdg1id 30715 ofcfval 31034 ccatmulgnn0dir 31491 signstf0 31517 curunc 34348 cncfiooicc 41637 dvcosax 41671 fourierdlem74 41926 fourierdlem75 41927 fourierdlem93 41945 smfsupxr 42551 smflimsuplem8 42562 |
Copyright terms: Public domain | W3C validator |