Theorem op1st 7941

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580  ⟨cop 4586  ∪ cuni 4863  dom cdm 5624  ‘cfv 6492  1^st c1st 7931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7933

This theorem is referenced by:  op1std  7943  op1stg  7945  1stval2  7950  fo1stres  7959  opreuopreu  7978  eloprabi  8007  xpmapenlem  9072  fseqenlem2  9935  archnq  10891  ruclem8  16162  idfu1st  17803  cofu1st  17807  xpccatid  18111  prf1st  18127  yonedalem21  18196  yonedalem22  18201  2ndcctbss  23399  upxp  23567  uptx  23569  cnheiborlem  24909  ovollb2lem  25445  ovolctb  25447  ovoliunlem2  25460  ovolshftlem1  25466  ovolscalem1  25470  ovolicc1  25473  addsqnreup  27410  2sqreuop  27429  2sqreuopnn  27430  2sqreuoplt  27431  2sqreuopltb  27432  2sqreuopnnlt  27433  2sqreuopnnltb  27434  precsexlem1  28203  precsexlem4  28206  ex-1st  30519  cnnvg  30753  cnnvs  30755  h2hva  31049  h2hsm  31050  hhssva  31332  hhsssm  31333  hhshsslem1  31342  gsumhashmul  33150  rlocf1  33355  fracfld  33390  eulerpartlemgvv  34533  eulerpartlemgh  34535  satfv0fvfmla0  35607  filnetlem3  36574  poimirlem17  37838  heiborlem8  38019  dvhvaddass  41357  dvhlveclem  41368  diblss  41430  aks6d1c3  42377  pellexlem5  43075  pellex  43077  dvnprodlem1  46190  hoicvr  46792  hoicvrrex  46800  ovn0lem  46809  ovnhoilem1  46845  gpgedgvtx0  48307  gpgedgvtx1  48308  gpg3kgrtriex  48335  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  eloprab1st2nd  49113  swapf1vala  49511  swapf2f1oaALT  49523  swapfcoa  49526  fuco21  49581  fucof21  49592  prcof1  49633  thincciso  49698