Theorem op2ndd 7985

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 6871	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nd 7983	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
5	1, 4	eqtrdi 2816	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ⟨cop 4591  ‘cfv 6525  2^nd c2nd 7973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fv 6533  df-2nd 7975

This theorem is referenced by:  2nd2val  8003  xp2nd  8007  sbcopeq1a  8034  csbopeq1a  8035  eloprabi  8048  mpomptsx  8049  dmmpossx  8051  fmpox  8052  ovmptss  8076  fmpoco  8078  df2nd2  8082  frxp  8110  xporderlem  8111  fnwelem  8115  fimaproj  8119  xpord2lem  8126  naddcllem  8650  xpf1o  9115  mapunen  9122  xpwdomg  9535  hsmexlem2  10399  nqereu  10902  uzrdgfni  13985  fsumcom2  15815  fprodcom2  16028  qredeu  16706  comfeq  17752  isfuncd  17912  cofucl  17935  funcres2b  17944  funcpropd  17949  xpcco2nd  18231  xpccatid  18234  1stf2  18239  2ndf2  18242  1stfcl  18243  2ndfcl  18244  prf2fval  18247  prfcl  18249  evlf2  18264  evlfcl  18268  curf12  18273  curf1cl  18274  curf2  18275  curfcl  18278  hof2fval  18301  hofcl  18305  txbas  23685  cnmpt2nd  23787  txhmeo  23921  ptuncnv  23925  ptunhmeo  23926  xpstopnlem1  23927  xkohmeo  23933  prdstmdd  24242  ucnimalem  24397  fmucndlem  24408  fsum2cn  24991  ovoliunlem1  25622  2sqreuop  27584  2sqreuopnn  27585  2sqreuoplt  27586  2sqreuopltb  27587  2sqreuopnnlt  27588  2sqreuopnnltb  27589  noseqrdgfn  28457  wlkl0  30627  fcnvgreu  32929  fsumiunle  33086  gsummpt2co  33281  gsumhashmul  33300  gsumwrd2dccatlem  33310  gsumwrd2dccat  33311  conjga  33403  elrgspnlem2  33476  elrgspnsubrunlem2  33481  mplvrpmga  33852  esumiun  34401  eulerpartlemgs2  34687  hgt750lemb  34960  satfv1  35726  satefvfmla0  35781  msubrsub  35889  msubco  35894  msubvrs  35923  nmulprop  36553  filnetlem4  36754  finixpnum  38116  poimirlem4  38135  poimirlem15  38146  poimirlem20  38151  poimirlem26  38157  heicant  38166  heiborlem4  38325  heiborlem6  38327  dicelvalN  41814  aks6d1c2p1  42747  aks6d1c3  42752  aks6d1c4  42753  aks6d1c6lem2  42800  aks6d1c6lem4  42802  aks6d1c7lem1  42809  fmpocos  42864  rmxypairf1o  43500  unxpwdom3  43684  fgraphxp  43793  elcnvlem  44189  dvnprodlem2  46519  etransclem46  46852  ovnsubaddlem1  47142  gpgvtxel2  48668  gpgvtx0  48673  gpgvtx1  48674  gpgedgvtx0  48681  gpgedgvtx1  48682  gpgvtxedg0  48683  gpgvtxedg1  48684  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem4  48739  pgnbgreunbgrlem5  48743  uspgrsprf  48766  uspgrsprf1  48767  dmmpossx2  48968  lmod1zr  49124  2arymaptf  49283  rrx2plordisom  49354  eloprab1st2nd  49497  funcf2lem  49710  oppf2  49769  tposcurf1  49928  reldmprcof2  50011  opf12  50033  setc1ocofval  50123