Theorem op1st 7993

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4594  ⟨cop 4600  ∪ cuni 4876  dom cdm 5662  ‘cfv 6537  1^st c1st 7983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-iota 6493  df-fun 6539  df-fv 6545  df-1st 7985

This theorem is referenced by:  op1std  7995  op1stg  7997  1stval2  8002  fo1stres  8011  opreuopreu  8030  eloprabi  8059  xpmapenlem  9131  fseqenlem2  10008  archnq  10964  ruclem8  16292  idfu1st  17935  cofu1st  17939  xpccatid  18243  prf1st  18259  yonedalem21  18328  yonedalem22  18333  2ndcctbss  23580  upxp  23748  uptx  23750  cnheiborlem  25081  ovollb2lem  25615  ovolctb  25617  ovoliunlem2  25630  ovolshftlem1  25636  ovolscalem1  25640  ovolicc1  25643  addsqnreup  27572  2sqreuop  27591  2sqreuopnn  27592  2sqreuoplt  27593  2sqreuopltb  27594  2sqreuopnnlt  27595  2sqreuopnnltb  27596  precsexlem1  28365  precsexlem4  28368  ex-1st  30735  cnnvg  30970  cnnvs  30972  h2hva  31266  h2hsm  31267  hhssva  31549  hhsssm  31550  hhshsslem1  31559  gsumhashmul  33327  rlocf1  33534  fracfld  33571  eulerpartlemgvv  34710  eulerpartlemgh  34712  satfv0fvfmla0  35803  filnetlem3  36779  poimirlem17  38175  heiborlem8  38356  dvhvaddass  41760  dvhlveclem  41771  diblss  41833  aks6d1c3  42779  pellexlem5  43451  pellex  43453  dvnprodlem1  46551  hoicvr  47153  hoicvrrex  47161  ovn0lem  47170  ovnhoilem1  47206  gpgedgvtx0  48714  gpgedgvtx1  48715  gpg3kgrtriex  48742  pgnioedg1  48761  pgnioedg2  48762  pgnioedg3  48763  pgnioedg4  48764  pgnioedg5  48765  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  pgnbgreunbgrlem5lem1  48773  pgnbgreunbgrlem5lem2  48774  pgnbgreunbgrlem5lem3  48775  eloprab1st2nd  49530  swapf1vala  49928  swapf2f1oaALT  49940  swapfcoa  49943  fuco21  49998  fucof21  50009  prcof1  50050  thincciso  50115