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 1928 | . 2 ⊢ (𝜑 → ∀𝑥 𝐴 = 𝐶) |
3 | mpteq12dva.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) | |
4 | 3 | ralrimiva 3184 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) |
5 | mpteq12f 5151 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | |
6 | 2, 4, 5 | syl2anc 586 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∀wal 1535 = wceq 1537 ∈ wcel 2114 ∀wral 3140 ↦ cmpt 5148 |
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-12 2177 ax-ext 2795 |
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 2802 df-cleq 2816 df-clel 2895 df-ral 3145 df-opab 5131 df-mpt 5149 |
This theorem is referenced by: mpteq12dvOLD 5154 pfxmpt 14042 reps 14134 repswccat 14150 cidpropd 16982 monpropd 17009 fucpropd 17249 curfpropd 17485 hofpropd 17519 yonffthlem 17534 ofco2 21062 pmatcollpw3fi1lem1 21396 rrxnm 23996 ushgredgedg 27013 ushgredgedgloop 27015 cshw1s2 30636 cycpm2tr 30763 sgnsv 30804 extdg1id 31055 ofcfval 31359 ccatmulgnn0dir 31814 signstf0 31840 curunc 34876 cncfiooicc 42184 dvcosax 42218 fourierdlem74 42472 fourierdlem75 42473 fourierdlem93 42491 smfsupxr 43097 smflimsuplem8 43108 |
Copyright terms: Public domain | W3C validator |