Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > op1sta | Structured version Visualization version GIF version |
Description: Extract the first member of an ordered pair. (See op2nda 6096 to extract the second member, op1stb 5360 for an alternate version, and op1st 7774 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.) |
Ref | Expression |
---|---|
cnvsn.1 | ⊢ 𝐴 ∈ V |
cnvsn.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
op1sta | ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvsn.2 | . . . 4 ⊢ 𝐵 ∈ V | |
2 | 1 | dmsnop 6084 | . . 3 ⊢ dom {〈𝐴, 𝐵〉} = {𝐴} |
3 | 2 | unieqi 4837 | . 2 ⊢ ∪ dom {〈𝐴, 𝐵〉} = ∪ {𝐴} |
4 | cnvsn.1 | . . 3 ⊢ 𝐴 ∈ V | |
5 | 4 | unisn 4846 | . 2 ⊢ ∪ {𝐴} = 𝐴 |
6 | 3, 5 | eqtri 2765 | 1 ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2110 Vcvv 3413 {csn 4546 〈cop 4552 ∪ cuni 4824 dom cdm 5556 |
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 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5197 ax-nul 5204 ax-pr 5327 |
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 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3415 df-dif 3874 df-un 3876 df-in 3878 df-ss 3888 df-nul 4243 df-if 4445 df-sn 4547 df-pr 4549 df-op 4553 df-uni 4825 df-br 5059 df-dm 5566 |
This theorem is referenced by: elxp4 7705 op1st 7774 fo1st 7786 f1stres 7790 xpassen 8744 xpdom2 8745 |
Copyright terms: Public domain | W3C validator |