MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  op1st Structured version   Visualization version   GIF version

Theorem op1st 7930
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
StepHypRef Expression
1 1stval 7924 . 2 (1st ‘⟨𝐴, 𝐵⟩) = dom {⟨𝐴, 𝐵⟩}
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op1sta 6178 . 2 dom {⟨𝐴, 𝐵⟩} = 𝐴
51, 4eqtri 2765 1 (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  Vcvv 3446  {csn 4587  cop 4593   cuni 4866  dom cdm 5634  cfv 6497  1st c1st 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-1st 7922
This theorem is referenced by:  op1std  7932  op1stg  7934  1stval2  7939  fo1stres  7948  opreuopreu  7967  eloprabi  7996  xpmapenlem  9089  fseqenlem2  9962  archnq  10917  ruclem8  16120  idfu1st  17766  cofu1st  17770  xpccatid  18077  prf1st  18093  yonedalem21  18163  yonedalem22  18168  2ndcctbss  22809  upxp  22977  uptx  22979  cnheiborlem  24320  ovollb2lem  24855  ovolctb  24857  ovoliunlem2  24870  ovolshftlem1  24876  ovolscalem1  24880  ovolicc1  24883  addsqnreup  26794  2sqreuop  26813  2sqreuopnn  26814  2sqreuoplt  26815  2sqreuopltb  26816  2sqreuopnnlt  26817  2sqreuopnnltb  26818  ex-1st  29391  cnnvg  29623  cnnvs  29625  h2hva  29919  h2hsm  29920  hhssva  30202  hhsssm  30203  hhshsslem1  30212  gsumhashmul  31901  eulerpartlemgvv  32979  eulerpartlemgh  32981  satfv0fvfmla0  34010  filnetlem3  34855  poimirlem17  36098  heiborlem8  36280  dvhvaddass  39563  dvhlveclem  39574  diblss  39636  pellexlem5  41159  pellex  41161  dvnprodlem1  44194  hoicvr  44796  hoicvrrex  44804  ovn0lem  44813  ovnhoilem1  44849  thincciso  47076
  Copyright terms: Public domain W3C validator