|   | 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 2141, ax-12 2177. (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 2748 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷)) | 
| 3 | 2 | pm5.32da 579 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷))) | 
| 4 | mpteq12dv.1 | . . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶) | |
| 5 | 4 | eleq2d 2827 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶)) | 
| 6 | 5 | anbi1d 631 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) | 
| 7 | 3, 6 | bitrd 279 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) | 
| 8 | 7 | opabbidv 5209 | . 2 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}) | 
| 9 | df-mpt 5226 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
| 10 | df-mpt 5226 | . 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)} | |
| 11 | 8, 9, 10 | 3eqtr4g 2802 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {copab 5205 ↦ cmpt 5225 | 
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-mpt 5226 | 
| This theorem is referenced by: mpteq12dv 5233 mpteq2dva 5242 pfxmpt 14716 reps 14808 repswccat 14824 cidpropd 17753 monpropd 17781 fucpropd 18025 curfpropd 18278 hofpropd 18312 yonffthlem 18327 ofco2 22457 pmatcollpw3fi1lem1 22792 rrxnm 25425 ushgredgedg 29246 ushgredgedgloop 29248 cshw1s2 32945 gsumpart 33060 gsumhashmul 33064 gsumwrd2dccat 33070 cycpm2tr 33139 sgnsv 33180 extdg1id 33716 ofcfval 34099 ccatmulgnn0dir 34557 signstf0 34583 curunc 37609 cncfiooicc 45909 dvcosax 45941 fourierdlem74 46195 fourierdlem75 46196 fourierdlem93 46214 smfsupxr 46831 smflimsuplem8 46842 | 
| Copyright terms: Public domain | W3C validator |