Theorem op2ndg 7940

Description: Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)

Assertion

Ref	Expression
op2ndg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Proof of Theorem op2ndg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4824	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6836	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4825	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6832	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2749	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3441	. . 3 ⊢ 𝑥 ∈ V
8		vex 3441	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7936	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3526	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4581  ‘cfv 6486  2^nd c2nd 7926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fv 6494  df-2nd 7928

This theorem is referenced by:  ot2ndg  7942  ot3rdg  7943  br2ndeqg  7950  2ndconst  8037  mposn  8039  curry1  8040  opco2  8060  xpmapenlem  9064  2ndinl  9828  2ndinr  9830  axdc4lem  10353  pinq  10825  addpipq  10835  mulpipq  10838  ordpipq  10840  swrdval  14553  ruclem1  16142  eucalg  16500  qnumdenbi  16657  setsstruct  17089  comffval  17607  oppccofval  17624  funcf2  17777  cofuval2  17796  resfval2  17802  resf2nd  17804  funcres  17805  isnat  17859  fucco  17874  homacd  17950  setcco  17992  catcco  18014  estrcco  18038  xpcco  18091  xpchom2  18094  xpcco2  18095  evlf2  18126  curfval  18131  curf1cl  18136  uncf1  18144  uncf2  18145  hof2fval  18163  yonedalem21  18181  yonedalem22  18186  mvmulfval  22458  imasdsf1olem  24289  ovolicc1  25445  ioombl1lem3  25489  ioombl1lem4  25490  addsqnreup  27382  addsval  27906  mulsval  28049  om2noseqrdg  28235  brcgr  28880  opiedgfv  28987  fsuppcurry1  32711  erlbrd  33237  rlocaddval  33242  rlocmulval  33243  fracerl  33279  sategoelfvb  35484  prv1n  35496  fvtransport  36097  bj-finsumval0  37350  poimirlem17  37697  poimirlem24  37704  poimirlem27  37707  dvhopvadd  41212  dvhopvsca  41221  dvhopaddN  41233  dvhopspN  41234  etransclem44  46400  gpgedgiov  48189  gpgedg2ov  48190  gpgedg2iv  48191  uspgrsprfo  48272  rngccoALTV  48395  ringccoALTV  48429  lmod1zr  48618  func2nd  49203  oppf1st2nd  49256  upfval3  49303  swapf2fval  49390  fucofval  49444  fuco112  49454  fuco21  49461  prcofvala  49502  lanfval  49738  ranfval  49739