Theorem op1st 7995

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3450  {csn 4584  ⟨cop 4590  ∪ cuni 4867  dom cdm 5655  ‘cfv 6533  1^st c1st 7985

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fv 6541  df-1st 7987

This theorem is used by:  op1std  7997  op1stg  7999  1stval2  8004  fo1stres  8013  opreuopreu  8032  eloprabi  8061  xpmapenlem  9143  fseqenlem2  10029  archnq  10990  ruclem8  16326  idfu1st  17969  cofu1st  17973  xpccatid  18277  prf1st  18293  yonedalem21  18362  yonedalem22  18367  2ndcctbss  23682  upxp  23850  uptx  23852  cnheiborlem  25183  ovollb2lem  25717  ovolctb  25719  ovoliunlem2  25732  ovolshftlem1  25738  ovolscalem1  25742  ovolicc1  25745  addsqnreup  27680  2sqreuop  27699  2sqreuopnn  27700  2sqreuoplt  27701  2sqreuopltb  27702  2sqreuopnnlt  27703  2sqreuopnnltb  27704  precsexlem1  28473  precsexlem4  28476  ex-1st  30925  cnnvg  31160  cnnvs  31162  h2hva  31456  h2hsm  31457  hhssva  31739  hhsssm  31740  hhshsslem1  31749  gsumhashmul  33508  rlocf1  33715  fracfld  33750  eulerpartlemgvv  34888  eulerpartlemgh  34890  satfv0fvfmla0  35993  filnetlem3  37000  poimirlem17  38387  heiborlem8  38569  dvhvaddass  41971  dvhlveclem  41982  diblss  42044  aks6d1c3  42990  pellexlem5  43675  pellex  43677  dvnprodlem1  46775  hoicvr  47377  hoicvrrex  47385  ovn0lem  47394  ovnhoilem1  47430  gpgedgvtx0  48978  gpgedgvtx1  48979  gpg3kgrtriex  49006  pgnioedg1  49025  pgnioedg2  49026  pgnioedg3  49027  pgnioedg4  49028  pgnioedg5  49029  pgnbgreunbgrlem2lem1  49031  pgnbgreunbgrlem2lem2  49032  pgnbgreunbgrlem2lem3  49033  pgnbgreunbgrlem5lem1  49037  pgnbgreunbgrlem5lem2  49038  pgnbgreunbgrlem5lem3  49039  eloprab1st2nd  49797  swapf1vala  50193  swapf2f1oaALT  50205  swapfcoa  50208  fuco21  50263  fucof21  50274  prcof1  50315  thincciso  50380