Theorem op2ndd 7709

Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
op1st.1	⊢ 𝐴 ∈ V
op1st.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
op2ndd	⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)

Proof of Theorem op2ndd

Step	Hyp	Ref	Expression
1		fveq2 6662	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nd 7707	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
5	1, 4	eqtrdi 2809	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ⟨cop 4531  ‘cfv 6339  2^nd c2nd 7697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-un 7464

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-iota 6298  df-fun 6341  df-fv 6347  df-2nd 7699

This theorem is referenced by:  2nd2val  7727  xp2nd  7731  sbcopeq1a  7757  csbopeq1a  7758  eloprabi  7770  mpomptsx  7771  dmmpossx  7773  fmpox  7774  ovmptss  7798  fmpoco  7800  df2nd2  7804  frxp  7830  xporderlem  7831  fnwelem  7835  fimaproj  7839  xpf1o  8706  mapunen  8713  xpwdomg  9087  hsmexlem2  9892  nqereu  10394  uzrdgfni  13380  fsumcom2  15182  fprodcom2  15391  qredeu  16059  comfeq  17039  isfuncd  17199  cofucl  17222  funcres2b  17231  funcpropd  17234  xpcco2nd  17506  xpccatid  17509  1stf2  17514  2ndf2  17517  1stfcl  17518  2ndfcl  17519  prf2fval  17522  prfcl  17524  evlf2  17539  evlfcl  17543  curf12  17548  curf1cl  17549  curf2  17550  curfcl  17553  hof2fval  17576  hofcl  17580  txbas  22272  cnmpt2nd  22374  txhmeo  22508  ptuncnv  22512  ptunhmeo  22513  xpstopnlem1  22514  xkohmeo  22520  prdstmdd  22829  ucnimalem  22986  fmucndlem  22997  fsum2cn  23577  ovoliunlem1  24207  2sqreuop  26150  2sqreuopnn  26151  2sqreuoplt  26152  2sqreuopltb  26153  2sqreuopnnlt  26154  2sqreuopnnltb  26155  wlkl0  28256  fcnvgreu  30538  fsumiunle  30671  gsummpt2co  30838  gsumhashmul  30846  esumiun  31585  eulerpartlemgs2  31870  hgt750lemb  32159  satfv1  32845  satefvfmla0  32900  msubrsub  33008  msubco  33013  msubvrs  33042  sbcoteq1a  33210  xpord2lem  33348  xpord3lem  33354  naddcllem  33420  filnetlem4  34145  finixpnum  35348  poimirlem4  35367  poimirlem15  35378  poimirlem20  35383  poimirlem26  35389  heicant  35398  heiborlem4  35558  heiborlem6  35560  dicelvalN  38780  rmxypairf1o  40253  unxpwdom3  40440  fgraphxp  40556  elcnvlem  40702  dvnprodlem2  42983  etransclem46  43316  ovnsubaddlem1  43603  uspgrsprf  44769  uspgrsprf1  44770  dmmpossx2  45133  lmod1zr  45295  2arymaptf  45459  rrx2plordisom  45530