Theorem op1st 8004

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 7998	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = ∪ dom {⟨𝐴, 𝐵⟩}
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1sta 6225	. 2 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
5	1, 4	eqtri 2757	1 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2107  Vcvv 3463  {csn 4606  ⟨cop 4612  ∪ cuni 4887  dom cdm 5665  ‘cfv 6541  1^st c1st 7994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-iota 6494  df-fun 6543  df-fv 6549  df-1st 7996

This theorem is referenced by:  op1std  8006  op1stg  8008  1stval2  8013  fo1stres  8022  opreuopreu  8041  eloprabi  8070  xpmapenlem  9166  fseqenlem2  10047  archnq  11002  ruclem8  16255  idfu1st  17895  cofu1st  17899  xpccatid  18203  prf1st  18219  yonedalem21  18288  yonedalem22  18293  2ndcctbss  23409  upxp  23577  uptx  23579  cnheiborlem  24922  ovollb2lem  25459  ovolctb  25461  ovoliunlem2  25474  ovolshftlem1  25480  ovolscalem1  25484  ovolicc1  25487  addsqnreup  27423  2sqreuop  27442  2sqreuopnn  27443  2sqreuoplt  27444  2sqreuopltb  27445  2sqreuopnnlt  27446  2sqreuopnnltb  27447  precsexlem1  28167  precsexlem4  28170  ex-1st  30391  cnnvg  30625  cnnvs  30627  h2hva  30921  h2hsm  30922  hhssva  31204  hhsssm  31205  hhshsslem1  31214  gsumhashmul  33003  rlocf1  33216  fracfld  33250  eulerpartlemgvv  34337  eulerpartlemgh  34339  satfv0fvfmla0  35377  filnetlem3  36340  poimirlem17  37603  heiborlem8  37784  dvhvaddass  41058  dvhlveclem  41069  diblss  41131  aks6d1c3  42083  pellexlem5  42807  pellex  42809  dvnprodlem1  45918  hoicvr  46520  hoicvrrex  46528  ovn0lem  46537  ovnhoilem1  46573  gpgedgvtx0  47977  gpgedgvtx1  47978  gpg3kgrtriex  48003  swapf1vala  48943  swapf2f1oaALT  48955  swapfcoa  48958  fuco21  49007  fucof21  49018  thincciso  49080