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

Theorem op2nd 7931
Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
Hypotheses
Ref Expression
op1st.1 𝐴 ∈ V
op1st.2 𝐵 ∈ V
Assertion
Ref Expression
op2nd (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵

Proof of Theorem op2nd
StepHypRef Expression
1 2ndval 7925 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = ran {⟨𝐴, 𝐵⟩}
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nda 6181 . 2 ran {⟨𝐴, 𝐵⟩} = 𝐵
51, 4eqtri 2765 1 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  Vcvv 3446  {csn 4587  cop 4593   cuni 4866  ran crn 5635  cfv 6497  2nd c2nd 7921
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-2nd 7923
This theorem is referenced by:  op2ndd  7933  op2ndg  7935  2ndval2  7940  fo2ndres  7949  opreuopreu  7967  eloprabi  7996  fo2ndf  8054  f1o2ndf1  8055  seqomlem1  8397  seqomlem2  8398  xpmapenlem  9089  fseqenlem2  9962  axdc4lem  10392  iunfo  10476  archnq  10917  om2uzrdg  13862  uzrdgsuci  13866  fsum2dlem  15656  fprod2dlem  15864  ruclem8  16120  ruclem11  16123  eucalglt  16462  idfu2nd  17764  idfucl  17768  cofu2nd  17772  cofucl  17775  xpccatid  18077  prf2nd  18094  curf2ndf  18137  yonedalem22  18168  gaid  19080  2ndcctbss  22809  upxp  22977  uptx  22979  txkgen  23006  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  wlkswwlksf1o  28827  clwlkclwwlkfo  28956  ex-2nd  29392  cnnvs  29625  cnnvnm  29626  h2hsm  29920  h2hnm  29921  hhsssm  30203  hhssnm  30204  2ndimaxp  31566  2ndresdju  31568  aciunf1lem  31581  gsumpart  31900  eulerpartlemgvv  32979  eulerpartlemgh  32981  satfv0fvfmla0  34010  sategoelfvb  34016  prv1n  34028  msubff1  34153  msubvrs  34157  poimirlem17  36098  heiborlem7  36279  heiborlem8  36280  dvhvaddass  39563  dvhlveclem  39574  diblss  39636  pellexlem5  41159  pellex  41161  dvnprodlem1  44194  hoicvr  44796  hoicvrrex  44804  ovn0lem  44813  ovnhoilem1  44849  ovnlecvr2  44858  ovolval5lem2  44901
  Copyright terms: Public domain W3C validator