Theorem op2ndd 7937

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3446  ⟨cop 4597  ‘cfv 6501  2^nd c2nd 7925

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fv 6509  df-2nd 7927

This theorem is referenced by:  2nd2val  7955  xp2nd  7959  sbcopeq1a  7986  csbopeq1a  7987  eloprabi  8000  mpomptsx  8001  dmmpossx  8003  fmpox  8004  ovmptss  8030  fmpoco  8032  df2nd2  8036  frxp  8063  xporderlem  8064  fnwelem  8068  fimaproj  8072  xpord2lem  8079  naddcllem  8627  xpf1o  9090  mapunen  9097  xpwdomg  9530  hsmexlem2  10372  nqereu  10874  uzrdgfni  13873  fsumcom2  15670  fprodcom2  15878  qredeu  16545  comfeq  17600  isfuncd  17765  cofucl  17788  funcres2b  17797  funcpropd  17801  xpcco2nd  18087  xpccatid  18090  1stf2  18095  2ndf2  18098  1stfcl  18099  2ndfcl  18100  prf2fval  18103  prfcl  18105  evlf2  18121  evlfcl  18125  curf12  18130  curf1cl  18131  curf2  18132  curfcl  18135  hof2fval  18158  hofcl  18162  txbas  22955  cnmpt2nd  23057  txhmeo  23191  ptuncnv  23195  ptunhmeo  23196  xpstopnlem1  23197  xkohmeo  23203  prdstmdd  23512  ucnimalem  23669  fmucndlem  23680  fsum2cn  24271  ovoliunlem1  24903  2sqreuop  26847  2sqreuopnn  26848  2sqreuoplt  26849  2sqreuopltb  26850  2sqreuopnnlt  26851  2sqreuopnnltb  26852  wlkl0  29374  fcnvgreu  31656  fsumiunle  31795  gsummpt2co  31960  gsumhashmul  31968  esumiun  32782  eulerpartlemgs2  33069  hgt750lemb  33358  satfv1  34044  satefvfmla0  34099  msubrsub  34207  msubco  34212  msubvrs  34241  filnetlem4  34929  finixpnum  36136  poimirlem4  36155  poimirlem15  36166  poimirlem20  36171  poimirlem26  36177  heicant  36186  heiborlem4  36346  heiborlem6  36348  dicelvalN  39714  aks6d1c2p1  40621  rmxypairf1o  41293  unxpwdom3  41480  fgraphxp  41596  elcnvlem  41995  dvnprodlem2  44308  etransclem46  44641  ovnsubaddlem1  44931  uspgrsprf  46168  uspgrsprf1  46169  dmmpossx2  46532  lmod1zr  46694  2arymaptf  46858  rrx2plordisom  46929  funcf2lem  47158