![]() |
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 2138, ax-12 2172. (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 2744 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷)) |
3 | 2 | pm5.32da 580 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷))) |
4 | mpteq12dv.1 | . . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶) | |
5 | 4 | eleq2d 2820 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶)) |
6 | 5 | anbi1d 631 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
7 | 3, 6 | bitrd 279 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
8 | 7 | opabbidv 5215 | . 2 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}) |
9 | df-mpt 5233 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
10 | df-mpt 5233 | . 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)} | |
11 | 8, 9, 10 | 3eqtr4g 2798 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 {copab 5211 ↦ cmpt 5232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-opab 5212 df-mpt 5233 |
This theorem is referenced by: mpteq12dv 5240 mpteq2dva 5249 pfxmpt 14628 reps 14720 repswccat 14736 cidpropd 17654 monpropd 17684 fucpropd 17930 curfpropd 18186 hofpropd 18220 yonffthlem 18235 ofco2 21953 pmatcollpw3fi1lem1 22288 rrxnm 24908 ushgredgedg 28486 ushgredgedgloop 28488 cshw1s2 32124 gsumpart 32207 gsumhashmul 32208 cycpm2tr 32278 sgnsv 32319 extdg1id 32742 ofcfval 33096 ccatmulgnn0dir 33553 signstf0 33579 curunc 36470 cncfiooicc 44610 dvcosax 44642 fourierdlem74 44896 fourierdlem75 44897 fourierdlem93 44915 smfsupxr 45532 smflimsuplem8 45543 |
Copyright terms: Public domain | W3C validator |