Theorem op1st 7979

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {csn 4592  ⟨cop 4598  ∪ cuni 4874  dom cdm 5641  ‘cfv 6514  1^st c1st 7969

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-1st 7971

This theorem is referenced by:  op1std  7981  op1stg  7983  1stval2  7988  fo1stres  7997  opreuopreu  8016  eloprabi  8045  xpmapenlem  9114  fseqenlem2  9985  archnq  10940  ruclem8  16212  idfu1st  17848  cofu1st  17852  xpccatid  18156  prf1st  18172  yonedalem21  18241  yonedalem22  18246  2ndcctbss  23349  upxp  23517  uptx  23519  cnheiborlem  24860  ovollb2lem  25396  ovolctb  25398  ovoliunlem2  25411  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  addsqnreup  27361  2sqreuop  27380  2sqreuopnn  27381  2sqreuoplt  27382  2sqreuopltb  27383  2sqreuopnnlt  27384  2sqreuopnnltb  27385  precsexlem1  28116  precsexlem4  28119  ex-1st  30380  cnnvg  30614  cnnvs  30616  h2hva  30910  h2hsm  30911  hhssva  31193  hhsssm  31194  hhshsslem1  31203  gsumhashmul  33008  rlocf1  33231  fracfld  33265  eulerpartlemgvv  34374  eulerpartlemgh  34376  satfv0fvfmla0  35407  filnetlem3  36375  poimirlem17  37638  heiborlem8  37819  dvhvaddass  41098  dvhlveclem  41109  diblss  41171  aks6d1c3  42118  pellexlem5  42828  pellex  42830  dvnprodlem1  45951  hoicvr  46553  hoicvrrex  46561  ovn0lem  46570  ovnhoilem1  46606  gpgedgvtx0  48056  gpgedgvtx1  48057  gpg3kgrtriex  48084  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  eloprab1st2nd  48860  swapf1vala  49259  swapf2f1oaALT  49271  swapfcoa  49274  fuco21  49329  fucof21  49340  prcof1  49381  thincciso  49446