Theorem op1st 7722

Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)

Hypotheses

Ref	Expression
op1st.1	⊢ 𝐴 ∈ V
op1st.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
op1st	⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴

Proof of Theorem op1st

Step	Hyp	Ref	Expression
1		1stval 7716	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = ∪ dom {⟨𝐴, 𝐵⟩}
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1sta 6057	. 2 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
5	1, 4	eqtri 2761	1 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3398  {csn 4516  ⟨cop 4522  ∪ cuni 4796  dom cdm 5525  ‘cfv 6339  1^st c1st 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-iota 6297  df-fun 6341  df-fv 6347  df-1st 7714

This theorem is referenced by:  op1std  7724  op1stg  7726  1stval2  7731  fo1stres  7740  opreuopreu  7759  eloprabi  7786  algrflem  7845  xpmapenlem  8734  fseqenlem2  9525  archnq  10480  ruclem8  15682  idfu1st  17254  cofu1st  17258  xpccatid  17554  prf1st  17570  yonedalem21  17639  yonedalem22  17644  2ndcctbss  22206  upxp  22374  uptx  22376  cnheiborlem  23706  ovollb2lem  24240  ovolctb  24242  ovoliunlem2  24255  ovolshftlem1  24261  ovolscalem1  24265  ovolicc1  24268  addsqnreup  26179  2sqreuop  26198  2sqreuopnn  26199  2sqreuoplt  26200  2sqreuopltb  26201  2sqreuopnnlt  26202  2sqreuopnnltb  26203  ex-1st  28381  cnnvg  28613  cnnvs  28615  h2hva  28909  h2hsm  28910  hhssva  29192  hhsssm  29193  hhshsslem1  29202  gsumhashmul  30893  eulerpartlemgvv  31913  eulerpartlemgh  31915  satfv0fvfmla0  32946  ot21std  33254  filnetlem3  34207  poimirlem17  35417  heiborlem8  35599  dvhvaddass  38734  dvhlveclem  38745  diblss  38807  pellexlem5  40227  pellex  40229  dvnprodlem1  43029  hoicvr  43628  hoicvrrex  43636  ovn0lem  43645  ovnhoilem1  43681