Theorem op1st 7932

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3436  {csn 4577  ⟨cop 4583  ∪ cuni 4858  dom cdm 5619  ‘cfv 6482  1^st c1st 7922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fv 6490  df-1st 7924

This theorem is referenced by:  op1std  7934  op1stg  7936  1stval2  7941  fo1stres  7950  opreuopreu  7969  eloprabi  7998  xpmapenlem  9061  fseqenlem2  9919  archnq  10874  ruclem8  16146  idfu1st  17786  cofu1st  17790  xpccatid  18094  prf1st  18110  yonedalem21  18179  yonedalem22  18184  2ndcctbss  23340  upxp  23508  uptx  23510  cnheiborlem  24851  ovollb2lem  25387  ovolctb  25389  ovoliunlem2  25402  ovolshftlem1  25408  ovolscalem1  25412  ovolicc1  25415  addsqnreup  27352  2sqreuop  27371  2sqreuopnn  27372  2sqreuoplt  27373  2sqreuopltb  27374  2sqreuopnnlt  27375  2sqreuopnnltb  27376  precsexlem1  28114  precsexlem4  28117  ex-1st  30388  cnnvg  30622  cnnvs  30624  h2hva  30918  h2hsm  30919  hhssva  31201  hhsssm  31202  hhshsslem1  31211  gsumhashmul  33014  rlocf1  33213  fracfld  33247  eulerpartlemgvv  34344  eulerpartlemgh  34346  satfv0fvfmla0  35386  filnetlem3  36354  poimirlem17  37617  heiborlem8  37798  dvhvaddass  41076  dvhlveclem  41087  diblss  41149  aks6d1c3  42096  pellexlem5  42806  pellex  42808  dvnprodlem1  45927  hoicvr  46529  hoicvrrex  46537  ovn0lem  46546  ovnhoilem1  46582  gpgedgvtx0  48045  gpgedgvtx1  48046  gpg3kgrtriex  48073  pgnioedg1  48092  pgnioedg2  48093  pgnioedg3  48094  pgnioedg4  48095  pgnioedg5  48096  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  pgnbgreunbgrlem5lem1  48104  pgnbgreunbgrlem5lem2  48105  pgnbgreunbgrlem5lem3  48106  eloprab1st2nd  48852  swapf1vala  49251  swapf2f1oaALT  49263  swapfcoa  49266  fuco21  49321  fucof21  49332  prcof1  49373  thincciso  49438