![]() |
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.) Remove dependency on ax-10 2129, ax-12 2166. (Revised by SN, 11-Nov-2024.) |
Ref | Expression |
---|---|
mpteq12dv.1 | ⊢ (𝜑 → 𝐴 = 𝐶) |
mpteq12dva.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
mpteq12dva | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq12dva.2 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) | |
2 | 1 | eqeq2d 2736 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷)) |
3 | 2 | pm5.32da 577 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷))) |
4 | mpteq12dv.1 | . . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶) | |
5 | 4 | eleq2d 2811 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶)) |
6 | 5 | anbi1d 629 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
7 | 3, 6 | bitrd 278 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
8 | 7 | opabbidv 5215 | . 2 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}) |
9 | df-mpt 5233 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
10 | df-mpt 5233 | . 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)} | |
11 | 8, 9, 10 | 3eqtr4g 2790 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 {copab 5211 ↦ cmpt 5232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-opab 5212 df-mpt 5233 |
This theorem is referenced by: mpteq12dv 5240 mpteq2dva 5249 pfxmpt 14664 reps 14756 repswccat 14772 cidpropd 17693 monpropd 17723 fucpropd 17972 curfpropd 18228 hofpropd 18262 yonffthlem 18277 ofco2 22397 pmatcollpw3fi1lem1 22732 rrxnm 25363 ushgredgedg 29114 ushgredgedgloop 29116 cshw1s2 32770 gsumpart 32859 gsumhashmul 32860 cycpm2tr 32932 sgnsv 32973 extdg1id 33486 ofcfval 33848 ccatmulgnn0dir 34305 signstf0 34331 curunc 37206 cncfiooicc 45420 dvcosax 45452 fourierdlem74 45706 fourierdlem75 45707 fourierdlem93 45725 smfsupxr 46342 smflimsuplem8 46353 |
Copyright terms: Public domain | W3C validator |