![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmsnopg | Structured version Visualization version GIF version |
Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
dmsnopg | ⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3451 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | vex 3451 | . . . . . 6 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | opth1 5436 | . . . . 5 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴) |
4 | 3 | exlimiv 1934 | . . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴) |
5 | opeq1 4834 | . . . . 5 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩) | |
6 | opeq2 4835 | . . . . . . 7 ⊢ (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩) | |
7 | 6 | eqeq1d 2735 | . . . . . 6 ⊢ (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)) |
8 | 7 | spcegv 3558 | . . . . 5 ⊢ (𝐵 ∈ 𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)) |
9 | 5, 8 | syl5 34 | . . . 4 ⊢ (𝐵 ∈ 𝑉 → (𝑥 = 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)) |
10 | 4, 9 | impbid2 225 | . . 3 ⊢ (𝐵 ∈ 𝑉 → (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴)) |
11 | 1 | eldm2 5861 | . . . 4 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩}) |
12 | opex 5425 | . . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ∈ V | |
13 | 12 | elsn 4605 | . . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
14 | 13 | exbii 1851 | . . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
15 | 11, 14 | bitri 275 | . . 3 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
16 | velsn 4606 | . . 3 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
17 | 10, 15, 16 | 3bitr4g 314 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴})) |
18 | 17 | eqrdv 2731 | 1 ⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∃wex 1782 ∈ wcel 2107 {csn 4590 ⟨cop 4596 dom cdm 5637 |
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 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-br 5110 df-dm 5647 |
This theorem is referenced by: dmsnopss 6170 dmpropg 6171 dmsnop 6172 rnsnopg 6177 fnsng 6557 funprg 6559 funtpg 6560 fntpg 6565 funsnfsupp 9337 s1dmALT 14506 setsval 17047 setsdm 17050 estrreslem2 18034 snstriedgval 28038 1loopgrvd0 28501 1hevtxdg0 28502 1hevtxdg1 28503 1egrvtxdg1 28506 p1evtxdeqlem 28509 wlkp1 28678 eupthp1 29209 trlsegvdeglem5 29217 cosnopne 31662 bnj96 33541 bnj535 33566 ovnovollem1 44987 |
Copyright terms: Public domain | W3C validator |