Theorem op2ndg 8003

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 4836	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6890	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4837	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6886	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 23	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2778	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3457	. . 3 ⊢ 𝑥 ∈ V
8		vex 3457	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7999	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3536	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4593  ‘cfv 6537  2^nd c2nd 7989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fv 6545  df-2nd 7991

This theorem is used by:  ot2ndg  8005  ot3rdg  8006  br2ndeqg  8013  2ndconst  8102  mposn  8104  curry1  8105  opco2  8125  xpmapenlem  9146  2ndinl  9937  2ndinr  9939  axdc4lem  10461  pinq  10940  addpipq  10950  mulpipq  10953  ordpipq  10955  swrdval  14715  ruclem1  16325  eucalg  16683  qnumdenbi  16841  setsstruct  17274  comffval  17793  oppccofval  17810  funcf2  17963  cofuval2  17982  resfval2  17988  resf2nd  17990  funcres  17991  isnat  18045  fucco  18060  homacd  18136  setcco  18178  catcco  18200  estrcco  18224  xpcco  18277  xpchom2  18280  xpcco2  18281  evlf2  18312  curfval  18317  curf1cl  18322  uncf1  18330  uncf2  18331  hof2fval  18349  yonedalem21  18367  yonedalem22  18372  mvmulfval  22770  imasdsf1olem  24605  ovolicc1  25750  ioombl1lem3  25794  ioombl1lem4  25795  addsqnreup  27687  addsval  28235  mulsval  28382  om2noseqrdg  28577  brcgr  29365  opiedgfv  29472  fsuppcurry1  33203  erlbrd  33711  erld2  33714  rlocaddval  33717  rlocmulval  33718  fracerl  33755  sategoelfvb  36006  prv1n  36018  fvtransport  36620  bj-finsumval0  38045  poimirlem17  38394  poimirlem24  38401  poimirlem27  38404  dvhopvadd  41974  dvhopvsca  41983  dvhopaddN  41995  dvhopspN  41996  etransclem44  47114  gpgedgiov  48989  gpgedg2ov  48990  gpgedg2iv  48991  uspgrsprfo  49072  rngccoALTV  49194  ringccoALTV  49228  lmod1zr  49431  func2nd  50012  oppf1st2nd  50065  upfval3  50112  swapf2fval  50199  fucofval  50253  fuco112  50263  fuco21  50270  prcofvala  50311  lanfval  50547  ranfval  50548