Theorem op1st 7436

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

Syntax hints:   = wceq 1656   ∈ wcel 2164  Vcvv 3414  {csn 4397  ⟨cop 4403  ∪ cuni 4658  dom cdm 5342  ‘cfv 6123  1^st c1st 7426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-iota 6086  df-fun 6125  df-fv 6131  df-1st 7428

This theorem is referenced by:  op1std  7438  op1stg  7440  1stval2  7445  fo1stres  7454  eloprabi  7495  algrflem  7550  xpmapenlem  8396  fseqenlem2  9161  archnq  10117  ruclem8  15340  idfu1st  16891  cofu1st  16895  xpccatid  17181  prf1st  17197  yonedalem21  17266  yonedalem22  17271  2ndcctbss  21629  upxp  21797  uptx  21799  cnheiborlem  23123  ovollb2lem  23654  ovolctb  23656  ovoliunlem2  23669  ovolshftlem1  23675  ovolscalem1  23679  ovolicc1  23682  wlknwwlksnsurOLD  27190  wlkwwlksurOLD  27198  clwlksfoclwwlkOLD  27432  ex-1st  27848  cnnvg  28077  cnnvs  28079  h2hva  28375  h2hsm  28376  hhssva  28658  hhsssm  28659  hhshsslem1  28668  eulerpartlemgvv  30972  eulerpartlemgh  30974  filnetlem3  32902  poimirlem17  33963  heiborlem8  34152  dvhvaddass  37165  dvhlveclem  37176  diblss  37238  pellexlem5  38234  pellex  38236  dvnprodlem1  40949  hoicvr  41549  hoicvrrex  41557  ovn0lem  41566  ovnhoilem1  41602