Theorem op1st 7939

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3431  {csn 4555  ⟨cop 4561  ∪ cuni 4838  dom cdm 5618  ‘cfv 6485  1^st c1st 7929

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fv 6493  df-1st 7931

This theorem is referenced by:  op1std  7941  op1stg  7943  1stval2  7948  fo1stres  7957  opreuopreu  7976  eloprabi  8005  xpmapenlem  9072  fseqenlem2  9938  archnq  10894  ruclem8  16195  idfu1st  17837  cofu1st  17841  xpccatid  18145  prf1st  18161  yonedalem21  18230  yonedalem22  18235  2ndcctbss  23438  upxp  23606  uptx  23608  cnheiborlem  24939  ovollb2lem  25473  ovolctb  25475  ovoliunlem2  25488  ovolshftlem1  25494  ovolscalem1  25498  ovolicc1  25501  addsqnreup  27424  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  precsexlem1  28217  precsexlem4  28220  ex-1st  30532  cnnvg  30767  cnnvs  30769  h2hva  31063  h2hsm  31064  hhssva  31346  hhsssm  31347  hhshsslem1  31356  gsumhashmul  33148  rlocf1  33354  fracfld  33392  eulerpartlemgvv  34560  eulerpartlemgh  34562  satfv0fvfmla0  35641  filnetlem3  36608  poimirlem17  38004  heiborlem8  38185  dvhvaddass  41589  dvhlveclem  41600  diblss  41662  aks6d1c3  42608  pellexlem5  43278  pellex  43280  dvnprodlem1  46389  hoicvr  46991  hoicvrrex  46999  ovn0lem  47008  ovnhoilem1  47044  gpgedgvtx0  48552  gpgedgvtx1  48553  gpg3kgrtriex  48580  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  eloprab1st2nd  49358  swapf1vala  49756  swapf2f1oaALT  49768  swapfcoa  49771  fuco21  49826  fucof21  49837  prcof1  49878  thincciso  49943