Theorem op1st 7950

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {csn 4567  ⟨cop 4573  ∪ cuni 4850  dom cdm 5631  ‘cfv 6498  1^st c1st 7940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fv 6506  df-1st 7942

This theorem is referenced by:  op1std  7952  op1stg  7954  1stval2  7959  fo1stres  7968  opreuopreu  7987  eloprabi  8016  xpmapenlem  9082  fseqenlem2  9947  archnq  10903  ruclem8  16204  idfu1st  17846  cofu1st  17850  xpccatid  18154  prf1st  18170  yonedalem21  18239  yonedalem22  18244  2ndcctbss  23420  upxp  23588  uptx  23590  cnheiborlem  24921  ovollb2lem  25455  ovolctb  25457  ovoliunlem2  25470  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  addsqnreup  27406  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  precsexlem1  28199  precsexlem4  28202  ex-1st  30514  cnnvg  30749  cnnvs  30751  h2hva  31045  h2hsm  31046  hhssva  31328  hhsssm  31329  hhshsslem1  31338  gsumhashmul  33128  rlocf1  33334  fracfld  33369  eulerpartlemgvv  34520  eulerpartlemgh  34522  satfv0fvfmla0  35595  filnetlem3  36562  poimirlem17  37958  heiborlem8  38139  dvhvaddass  41543  dvhlveclem  41554  diblss  41616  aks6d1c3  42562  pellexlem5  43261  pellex  43263  dvnprodlem1  46374  hoicvr  46976  hoicvrrex  46984  ovn0lem  46993  ovnhoilem1  47029  gpgedgvtx0  48537  gpgedgvtx1  48538  gpg3kgrtriex  48565  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  eloprab1st2nd  49343  swapf1vala  49741  swapf2f1oaALT  49753  swapfcoa  49756  fuco21  49811  fucof21  49822  prcof1  49863  thincciso  49928