![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmsnop | 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 NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
dmsnop.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
dmsnop | ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmsnop.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | dmsnopg 6169 | . 2 ⊢ (𝐵 ∈ V → dom {⟨𝐴, 𝐵⟩} = {𝐴}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∈ wcel 2107 Vcvv 3447 {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: dmtpop 6174 dmsnsnsn 6176 op1sta 6181 snres0 6254 funtp 6562 funopdmsn 7100 frrlem14 8234 wfrlem13OLD 8271 wfrlem16OLD 8274 tfrlem10 8337 ac6sfi 9237 dcomex 10391 axdc3lem4 10397 cnfldfunALT 20832 cnfldfunALTOLD 20833 noextend 27037 nosupbday 27076 nosupbnd1 27085 nosupbnd2 27087 noinfbday 27091 noinfbnd1 27100 noinfbnd2 27102 bnj1416 33715 bnj1421 33718 fineqvac 33762 subfacp1lem2a 33838 subfacp1lem5 33842 |
Copyright terms: Public domain | W3C validator |