Theorem op1sta 5341

Description: Extract the first member of an ordered pair. (See op2nda 5344 to extract the second member, op1stb 4585 for an alternate version, and op1st 6591 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)

Hypotheses

Ref	Expression
cnvsn.1
cnvsn.2

Assertion

Ref	Expression
op1sta

Proof of Theorem op1sta

Step	Hyp	Ref	Expression
1		cnvsn.2	. . . 4
2	1	dmsnop 5333	. . 3
3	2	unieqi 4126	. 2
4		cnvsn.1	. . 3
5	4	unisn 4132	. 2
6	3, 5	eqtri 2509	1

Syntax hints:  =wceq 1670  e.wcel 1732  cvv 3015  {csn 3909  <.cop 3912  U.cuni 4117  domcdm 4862

This theorem is referenced by:  elxp4  6530  op1st  6591  fo1st  6602  f1stres  6604  xpassen  7367  xpdom2  7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-dm 4872