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 3402 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | vex 3402 | . . . . . 6 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | opth1 5344 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑥 = 𝐴) |
4 | 3 | exlimiv 1938 | . . . 4 ⊢ (∃𝑦〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑥 = 𝐴) |
5 | opeq1 4770 | . . . . 5 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝐵〉 = 〈𝐴, 𝐵〉) | |
6 | opeq2 4771 | . . . . . . 7 ⊢ (𝑦 = 𝐵 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝐵〉) | |
7 | 6 | eqeq1d 2738 | . . . . . 6 ⊢ (𝑦 = 𝐵 → (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 ↔ 〈𝑥, 𝐵〉 = 〈𝐴, 𝐵〉)) |
8 | 7 | spcegv 3502 | . . . . 5 ⊢ (𝐵 ∈ 𝑉 → (〈𝑥, 𝐵〉 = 〈𝐴, 𝐵〉 → ∃𝑦〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉)) |
9 | 5, 8 | syl5 34 | . . . 4 ⊢ (𝐵 ∈ 𝑉 → (𝑥 = 𝐴 → ∃𝑦〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉)) |
10 | 4, 9 | impbid2 229 | . . 3 ⊢ (𝐵 ∈ 𝑉 → (∃𝑦〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 ↔ 𝑥 = 𝐴)) |
11 | 1 | eldm2 5755 | . . . 4 ⊢ (𝑥 ∈ dom {〈𝐴, 𝐵〉} ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}) |
12 | opex 5333 | . . . . . 6 ⊢ 〈𝑥, 𝑦〉 ∈ V | |
13 | 12 | elsn 4542 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉} ↔ 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
14 | 13 | exbii 1855 | . . . 4 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉} ↔ ∃𝑦〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
15 | 11, 14 | bitri 278 | . . 3 ⊢ (𝑥 ∈ dom {〈𝐴, 𝐵〉} ↔ ∃𝑦〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
16 | velsn 4543 | . . 3 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
17 | 10, 15, 16 | 3bitr4g 317 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ dom {〈𝐴, 𝐵〉} ↔ 𝑥 ∈ {𝐴})) |
18 | 17 | eqrdv 2734 | 1 ⊢ (𝐵 ∈ 𝑉 → dom {〈𝐴, 𝐵〉} = {𝐴}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∃wex 1787 ∈ wcel 2112 {csn 4527 〈cop 4533 dom cdm 5536 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-br 5040 df-dm 5546 |
This theorem is referenced by: dmsnopss 6057 dmpropg 6058 dmsnop 6059 rnsnopg 6064 fnsng 6410 funprg 6412 funtpg 6413 fntpg 6418 funsnfsupp 8987 s1dmALT 14131 setsval 16695 setsdm 16699 estrreslem2 17599 snstriedgval 27083 1loopgrvd0 27546 1hevtxdg0 27547 1hevtxdg1 27548 1egrvtxdg1 27551 p1evtxdeqlem 27554 wlkp1 27723 eupthp1 28253 trlsegvdeglem5 28261 cosnopne 30701 bnj96 32512 bnj535 32537 ovnovollem1 43812 |
Copyright terms: Public domain | W3C validator |