Theorem op2ndd 7692

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 6663	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nd 7690	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
5	1, 4	syl6eq 2870	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1531   ∈ wcel 2108  Vcvv 3493  ⟨cop 4565  ‘cfv 6348  2^nd c2nd 7680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fv 6356  df-2nd 7682

This theorem is referenced by:  2nd2val  7710  xp2nd  7714  sbcopeq1a  7740  csbopeq1a  7741  eloprabi  7753  mpomptsx  7754  dmmpossx  7756  fmpox  7757  ovmptss  7780  fmpoco  7782  df2nd2  7786  frxp  7812  xporderlem  7813  fnwelem  7817  fimaproj  7821  xpf1o  8671  mapunen  8678  xpwdomg  9041  hsmexlem2  9841  nqereu  10343  uzrdgfni  13318  fsumcom2  15121  fprodcom2  15330  qredeu  15994  comfeq  16968  isfuncd  17127  cofucl  17150  funcres2b  17159  funcpropd  17162  xpcco2nd  17427  xpccatid  17430  1stf2  17435  2ndf2  17438  1stfcl  17439  2ndfcl  17440  prf2fval  17443  prfcl  17445  evlf2  17460  evlfcl  17464  curf12  17469  curf1cl  17470  curf2  17471  curfcl  17474  hof2fval  17497  hofcl  17501  txbas  22167  cnmpt2nd  22269  txhmeo  22403  ptuncnv  22407  ptunhmeo  22408  xpstopnlem1  22409  xkohmeo  22415  prdstmdd  22724  ucnimalem  22881  fmucndlem  22892  fsum2cn  23471  ovoliunlem1  24095  2sqreuop  26030  2sqreuopnn  26031  2sqreuoplt  26032  2sqreuopltb  26033  2sqreuopnnlt  26034  2sqreuopnnltb  26035  wlkl0  28138  fcnvgreu  30410  fsumiunle  30538  gsummpt2co  30679  esumiun  31346  eulerpartlemgs2  31631  hgt750lemb  31920  satfv1  32603  satefvfmla0  32658  msubrsub  32766  msubco  32771  msubvrs  32800  filnetlem4  33722  finixpnum  34869  poimirlem4  34888  poimirlem15  34899  poimirlem20  34904  poimirlem26  34910  heicant  34919  heiborlem4  35084  heiborlem6  35086  dicelvalN  38306  rmxypairf1o  39499  unxpwdom3  39686  fgraphxp  39802  elcnvlem  39952  dvnprodlem2  42222  etransclem46  42556  ovnsubaddlem1  42843  uspgrsprf  44012  uspgrsprf1  44013  dmmpossx2  44376  lmod1zr  44539  rrx2plordisom  44701