Theorem op1st 8009

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {csn 4584  ⟨cop 4590  ∪ cuni 4867  dom cdm 5651  ‘cfv 6538  1^st c1st 7999

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001

This theorem is used by:  op1std  8011  op1stg  8013  1stval2  8018  fo1stres  8027  opreuopreu  8046  eloprabi  8074  xpmapenlem  9163  fseqenlem2  10104  archnq  11065  ruclem8  16405  idfu1st  18054  cofu1st  18058  xpccatid  18362  prf1st  18378  yonedalem21  18447  yonedalem22  18452  2ndcctbss  23774  upxp  23942  uptx  23944  cnheiborlem  25275  ovollb2lem  25809  ovolctb  25811  ovoliunlem2  25824  ovolshftlem1  25830  ovolscalem1  25834  ovolicc1  25837  addsqnreup  27770  2sqreuop  27789  2sqreuopnn  27790  2sqreuoplt  27791  2sqreuopltb  27792  2sqreuopnnlt  27793  2sqreuopnnltb  27794  precsexlem1  28593  precsexlem4  28596  ex-1st  31045  cnnvg  31280  cnnvs  31282  h2hva  31576  h2hsm  31577  hhssva  31859  hhsssm  31860  hhshsslem1  31869  gsumhashmul  33628  rlocf1  33835  fracfld  33870  eulerpartlemgvv  35008  eulerpartlemgh  35010  satfv0fvfmla0  36178  filnetlem3  37168  poimirlem17  38555  heiborlem8  38752  dvhvaddass  42154  dvhlveclem  42165  diblss  42227  aks6d1c3  43173  pellexlem5  43839  pellex  43841  dvnprodlem1  46955  hoicvr  47557  hoicvrrex  47565  ovn0lem  47574  ovnhoilem1  47610  gpgedgvtx0  49158  gpgedgvtx1  49159  gpg3kgrtriex  49186  pgnioedg1  49205  pgnioedg2  49206  pgnioedg3  49207  pgnioedg4  49208  pgnioedg5  49209  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  pgnbgreunbgrlem5lem1  49217  pgnbgreunbgrlem5lem2  49218  pgnbgreunbgrlem5lem3  49219  eloprab1st2nd  49977  swapf1vala  50373  swapf2f1oaALT  50385  swapfcoa  50388  fuco21  50443  fucof21  50454  prcof1  50495  thincciso  50560