Theorem op2ndd 7982

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ⟨cop 4598  ‘cfv 6514  2^nd c2nd 7970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-2nd 7972

This theorem is referenced by:  2nd2val  8000  xp2nd  8004  sbcopeq1a  8031  csbopeq1a  8032  eloprabi  8045  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  fmpoco  8077  df2nd2  8081  frxp  8108  xporderlem  8109  fnwelem  8113  fimaproj  8117  xpord2lem  8124  naddcllem  8643  xpf1o  9109  mapunen  9116  xpwdomg  9545  hsmexlem2  10387  nqereu  10889  uzrdgfni  13930  fsumcom2  15747  fprodcom2  15957  qredeu  16635  comfeq  17674  isfuncd  17834  cofucl  17857  funcres2b  17866  funcpropd  17871  xpcco2nd  18153  xpccatid  18156  1stf2  18161  2ndf2  18164  1stfcl  18165  2ndfcl  18166  prf2fval  18169  prfcl  18171  evlf2  18186  evlfcl  18190  curf12  18195  curf1cl  18196  curf2  18197  curfcl  18200  hof2fval  18223  hofcl  18227  txbas  23461  cnmpt2nd  23563  txhmeo  23697  ptuncnv  23701  ptunhmeo  23702  xpstopnlem1  23703  xkohmeo  23709  prdstmdd  24018  ucnimalem  24174  fmucndlem  24185  fsum2cn  24769  ovoliunlem1  25410  2sqreuop  27380  2sqreuopnn  27381  2sqreuoplt  27382  2sqreuopltb  27383  2sqreuopnnlt  27384  2sqreuopnnltb  27385  noseqrdgfn  28207  wlkl0  30303  fcnvgreu  32604  fsumiunle  32761  gsummpt2co  32995  gsumhashmul  33008  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  conjga  33134  elrgspnlem2  33201  elrgspnsubrunlem2  33206  esumiun  34091  eulerpartlemgs2  34378  hgt750lemb  34654  satfv1  35357  satefvfmla0  35412  msubrsub  35520  msubco  35525  msubvrs  35554  filnetlem4  36376  finixpnum  37606  poimirlem4  37625  poimirlem15  37636  poimirlem20  37641  poimirlem26  37647  heicant  37656  heiborlem4  37815  heiborlem6  37817  dicelvalN  41179  aks6d1c2p1  42113  aks6d1c3  42118  aks6d1c4  42119  aks6d1c6lem2  42166  aks6d1c6lem4  42168  aks6d1c7lem1  42175  fmpocos  42229  rmxypairf1o  42907  unxpwdom3  43091  fgraphxp  43200  elcnvlem  43597  dvnprodlem2  45952  etransclem46  46285  ovnsubaddlem1  46575  gpgvtxel2  48043  gpgvtx0  48048  gpgvtx1  48049  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  uspgrsprf  48138  uspgrsprf1  48139  dmmpossx2  48329  lmod1zr  48486  2arymaptf  48645  rrx2plordisom  48716  eloprab1st2nd  48860  funcf2lem  49074  oppf2  49133  tposcurf1  49292  reldmprcof2  49375  opf12  49397  setc1ocofval  49487