Theorem op1st 8022

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {csn 4626  ⟨cop 4632  ∪ cuni 4907  dom cdm 5685  ‘cfv 6561  1^st c1st 8012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014

This theorem is referenced by:  op1std  8024  op1stg  8026  1stval2  8031  fo1stres  8040  opreuopreu  8059  eloprabi  8088  xpmapenlem  9184  fseqenlem2  10065  archnq  11020  ruclem8  16273  idfu1st  17924  cofu1st  17928  xpccatid  18233  prf1st  18249  yonedalem21  18318  yonedalem22  18323  2ndcctbss  23463  upxp  23631  uptx  23633  cnheiborlem  24986  ovollb2lem  25523  ovolctb  25525  ovoliunlem2  25538  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  addsqnreup  27487  2sqreuop  27506  2sqreuopnn  27507  2sqreuoplt  27508  2sqreuopltb  27509  2sqreuopnnlt  27510  2sqreuopnnltb  27511  precsexlem1  28231  precsexlem4  28234  ex-1st  30463  cnnvg  30697  cnnvs  30699  h2hva  30993  h2hsm  30994  hhssva  31276  hhsssm  31277  hhshsslem1  31286  gsumhashmul  33064  rlocf1  33277  fracfld  33310  eulerpartlemgvv  34378  eulerpartlemgh  34380  satfv0fvfmla0  35418  filnetlem3  36381  poimirlem17  37644  heiborlem8  37825  dvhvaddass  41099  dvhlveclem  41110  diblss  41172  aks6d1c3  42124  pellexlem5  42844  pellex  42846  dvnprodlem1  45961  hoicvr  46563  hoicvrrex  46571  ovn0lem  46580  ovnhoilem1  46616  gpgedgvtx0  48019  gpgedgvtx1  48020  gpg3kgrtriex  48045  swapf1vala  48972  swapf2f1oaALT  48984  swapfcoa  48987  fuco21  49031  fucof21  49042  thincciso  49102