Theorem op1st 7976

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589  ⟨cop 4595  ∪ cuni 4871  dom cdm 5638  ‘cfv 6511  1^st c1st 7966

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-1st 7968

This theorem is referenced by:  op1std  7978  op1stg  7980  1stval2  7985  fo1stres  7994  opreuopreu  8013  eloprabi  8042  xpmapenlem  9108  fseqenlem2  9978  archnq  10933  ruclem8  16205  idfu1st  17841  cofu1st  17845  xpccatid  18149  prf1st  18165  yonedalem21  18234  yonedalem22  18239  2ndcctbss  23342  upxp  23510  uptx  23512  cnheiborlem  24853  ovollb2lem  25389  ovolctb  25391  ovoliunlem2  25404  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  addsqnreup  27354  2sqreuop  27373  2sqreuopnn  27374  2sqreuoplt  27375  2sqreuopltb  27376  2sqreuopnnlt  27377  2sqreuopnnltb  27378  precsexlem1  28109  precsexlem4  28112  ex-1st  30373  cnnvg  30607  cnnvs  30609  h2hva  30903  h2hsm  30904  hhssva  31186  hhsssm  31187  hhshsslem1  31196  gsumhashmul  33001  rlocf1  33224  fracfld  33258  eulerpartlemgvv  34367  eulerpartlemgh  34369  satfv0fvfmla0  35400  filnetlem3  36368  poimirlem17  37631  heiborlem8  37812  dvhvaddass  41091  dvhlveclem  41102  diblss  41164  aks6d1c3  42111  pellexlem5  42821  pellex  42823  dvnprodlem1  45944  hoicvr  46546  hoicvrrex  46554  ovn0lem  46563  ovnhoilem1  46599  gpgedgvtx0  48052  gpgedgvtx1  48053  gpg3kgrtriex  48080  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  eloprab1st2nd  48856  swapf1vala  49255  swapf2f1oaALT  49267  swapfcoa  49270  fuco21  49325  fucof21  49336  prcof1  49377  thincciso  49442