Theorem op1st 8000

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457  {csn 4591  ⟨cop 4597  ∪ cuni 4874  dom cdm 5663  ‘cfv 6540  1^st c1st 7990

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fv 6548  df-1st 7992

This theorem is used by:  op1std  8002  op1stg  8004  1stval2  8009  fo1stres  8018  opreuopreu  8037  eloprabi  8066  xpmapenlem  9139  fseqenlem2  10025  archnq  10980  ruclem8  16315  idfu1st  17958  cofu1st  17962  xpccatid  18266  prf1st  18282  yonedalem21  18351  yonedalem22  18356  2ndcctbss  23663  upxp  23831  uptx  23833  cnheiborlem  25164  ovollb2lem  25698  ovolctb  25700  ovoliunlem2  25713  ovolshftlem1  25719  ovolscalem1  25723  ovolicc1  25726  addsqnreup  27658  2sqreuop  27677  2sqreuopnn  27678  2sqreuoplt  27679  2sqreuopltb  27680  2sqreuopnnlt  27681  2sqreuopnnltb  27682  precsexlem1  28451  precsexlem4  28454  ex-1st  30866  cnnvg  31101  cnnvs  31103  h2hva  31397  h2hsm  31398  hhssva  31680  hhsssm  31681  hhshsslem1  31690  gsumhashmul  33451  rlocf1  33658  fracfld  33693  eulerpartlemgvv  34831  eulerpartlemgh  34833  satfv0fvfmla0  35942  filnetlem3  36948  poimirlem17  38345  heiborlem8  38527  dvhvaddass  41929  dvhlveclem  41940  diblss  42002  aks6d1c3  42948  pellexlem5  43618  pellex  43620  dvnprodlem1  46718  hoicvr  47320  hoicvrrex  47328  ovn0lem  47337  ovnhoilem1  47373  gpgedgvtx0  48884  gpgedgvtx1  48885  gpg3kgrtriex  48912  pgnioedg1  48931  pgnioedg2  48932  pgnioedg3  48933  pgnioedg4  48934  pgnioedg5  48935  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  pgnbgreunbgrlem2lem3  48939  pgnbgreunbgrlem5lem1  48943  pgnbgreunbgrlem5lem2  48944  pgnbgreunbgrlem5lem3  48945  eloprab1st2nd  49703  swapf1vala  50101  swapf2f1oaALT  50113  swapfcoa  50116  fuco21  50171  fucof21  50182  prcof1  50223  thincciso  50288