![]() |
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 2139, ax-12 2175. (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 2746 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷)) |
3 | 2 | pm5.32da 579 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷))) |
4 | mpteq12dv.1 | . . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶) | |
5 | 4 | eleq2d 2825 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶)) |
6 | 5 | anbi1d 631 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
7 | 3, 6 | bitrd 279 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷))) |
8 | 7 | opabbidv 5214 | . 2 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}) |
9 | df-mpt 5232 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
10 | df-mpt 5232 | . 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)} | |
11 | 8, 9, 10 | 3eqtr4g 2800 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 {copab 5210 ↦ cmpt 5231 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-opab 5211 df-mpt 5232 |
This theorem is referenced by: mpteq12dv 5239 mpteq2dva 5248 pfxmpt 14713 reps 14805 repswccat 14821 cidpropd 17755 monpropd 17785 fucpropd 18034 curfpropd 18290 hofpropd 18324 yonffthlem 18339 ofco2 22473 pmatcollpw3fi1lem1 22808 rrxnm 25439 ushgredgedg 29261 ushgredgedgloop 29263 cshw1s2 32930 gsumpart 33043 gsumhashmul 33047 gsumwrd2dccat 33053 cycpm2tr 33122 sgnsv 33163 extdg1id 33691 ofcfval 34079 ccatmulgnn0dir 34536 signstf0 34562 curunc 37589 cncfiooicc 45850 dvcosax 45882 fourierdlem74 46136 fourierdlem75 46137 fourierdlem93 46155 smfsupxr 46772 smflimsuplem8 46783 |
Copyright terms: Public domain | W3C validator |