MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  op1sta Structured version   Visualization version   GIF version

Theorem op1sta 6093
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.)
Hypotheses
Ref Expression
cnvsn.1 𝐴 ∈ V
cnvsn.2 𝐵 ∈ V
Assertion
Ref Expression
op1sta dom {⟨𝐴, 𝐵⟩} = 𝐴

Proof of Theorem op1sta
StepHypRef Expression
1 cnvsn.2 . . . 4 𝐵 ∈ V
21dmsnop 6084 . . 3 dom {⟨𝐴, 𝐵⟩} = {𝐴}
32unieqi 4837 . 2 dom {⟨𝐴, 𝐵⟩} = {𝐴}
4 cnvsn.1 . . 3 𝐴 ∈ V
54unisn 4846 . 2 {𝐴} = 𝐴
63, 5eqtri 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