![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpoeq123dva | Structured version Visualization version GIF version |
Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Ref | Expression |
---|---|
mpoeq123dv.1 | ⊢ (𝜑 → 𝐴 = 𝐷) |
mpoeq123dva.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
mpoeq123dva.3 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
Ref | Expression |
---|---|
mpoeq123dva | ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoeq123dva.3 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) | |
2 | 1 | eqeq2d 2748 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐹)) |
3 | 2 | pm5.32da 579 | . . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐹))) |
4 | mpoeq123dva.2 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) | |
5 | 4 | eleq2d 2823 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐸)) |
6 | 5 | pm5.32da 579 | . . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐸))) |
7 | mpoeq123dv.1 | . . . . . . . 8 ⊢ (𝜑 → 𝐴 = 𝐷) | |
8 | 7 | eleq2d 2823 | . . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐷)) |
9 | 8 | anbi1d 630 | . . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐸) ↔ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸))) |
10 | 6, 9 | bitrd 278 | . . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸))) |
11 | 10 | anbi1d 630 | . . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐹) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹))) |
12 | 3, 11 | bitrd 278 | . . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹))) |
13 | 12 | oprabbidv 7417 | . 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹)}) |
14 | df-mpo 7356 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
15 | df-mpo 7356 | . 2 ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹)} | |
16 | 13, 14, 15 | 3eqtr4g 2802 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {coprab 7352 ∈ cmpo 7353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-oprab 7355 df-mpo 7356 |
This theorem is referenced by: mpoeq123dv 7426 natpropd 17825 fucpropd 17826 curfpropd 18082 hofpropd 18116 rrxdsfi 24727 istrkgl 27229 eengv 27757 elntg 27762 submat1n 32198 rrxtopnfi 44429 rngcifuestrc 46196 funcrngcsetc 46197 funcrngcsetcALT 46198 funcringcsetc 46234 eenglngeehlnm 46726 |
Copyright terms: Public domain | W3C validator |