Theorem op2ndg 8001

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 4842	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6892	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4843	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6888	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 23	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2785	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3467	. . 3 ⊢ 𝑥 ∈ V
8		vex 3467	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7997	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3547	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ⟨cop 4600  ‘cfv 6539  2^nd c2nd 7987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5273  ax-pr 5407  ax-un 7735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-iota 6495  df-fun 6541  df-fv 6547  df-2nd 7989

This theorem is referenced by:  ot2ndg  8003  ot3rdg  8004  br2ndeqg  8011  2ndconst  8098  mposn  8100  curry1  8101  opco2  8121  xpmapenlem  9134  2ndinl  9916  2ndinr  9918  axdc4lem  10441  pinq  10914  addpipq  10924  mulpipq  10927  ordpipq  10929  swrdval  14683  ruclem1  16289  eucalg  16647  qnumdenbi  16805  setsstruct  17238  comffval  17757  oppccofval  17774  funcf2  17927  cofuval2  17946  resfval2  17952  resf2nd  17954  funcres  17955  isnat  18009  fucco  18024  homacd  18100  setcco  18142  catcco  18164  estrcco  18188  xpcco  18241  xpchom2  18244  xpcco2  18245  evlf2  18276  curfval  18281  curf1cl  18286  uncf1  18294  uncf2  18295  hof2fval  18313  yonedalem21  18331  yonedalem22  18336  mvmulfval  22670  imasdsf1olem  24501  ovolicc1  25646  ioombl1lem3  25690  ioombl1lem4  25691  addsqnreup  27575  addsval  28123  mulsval  28270  om2noseqrdg  28465  brcgr  29193  opiedgfv  29300  fsuppcurry1  33012  erlbrd  33526  erld2  33529  rlocaddval  33532  rlocmulval  33533  fracerl  33572  sategoelfvb  35846  prv1n  35858  fvtransport  36459  bj-finsumval0  37854  poimirlem17  38213  poimirlem24  38220  poimirlem27  38223  dvhopvadd  41794  dvhopvsca  41803  dvhopaddN  41815  dvhopspN  41816  etransclem44  46921  gpgedgiov  48756  gpgedg2ov  48757  gpgedg2iv  48758  uspgrsprfo  48839  rngccoALTV  48962  ringccoALTV  48996  lmod1zr  49195  func2nd  49778  oppf1st2nd  49831  upfval3  49878  swapf2fval  49965  fucofval  50019  fuco112  50029  fuco21  50036  prcofvala  50077  lanfval  50313  ranfval  50314