Theorem op2ndg 7181

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

Assertion

Ref	Expression
op2ndg	|- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )

Proof of Theorem op2ndg

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4402	. . . 4 |- ( x = A -> <. x , y >. = <. A , y >. )
2	1	fveq2d 6195	. . 3 |- ( x = A -> ( 2nd ` <. x , y >. ) = ( 2nd ` <. A , y >. ) )
3	2	eqeq1d 2624	. 2 |- ( x = A -> ( ( 2nd ` <. x , y >. ) = y <-> ( 2nd ` <. A , y >. ) = y ) )
4		opeq2 4403	. . . 4 |- ( y = B -> <. A , y >. = <. A , B >. )
5	4	fveq2d 6195	. . 3 |- ( y = B -> ( 2nd ` <. A , y >. ) = ( 2nd ` <. A , B >. ) )
6		id 22	. . 3 |- ( y = B -> y = B )
7	5, 6	eqeq12d 2637	. 2 |- ( y = B -> ( ( 2nd ` <. A , y >. ) = y <-> ( 2nd ` <. A , B >. ) = B ) )
8		vex 3203	. . 3 |- x e. _V
9		vex 3203	. . 3 |- y e. _V
10	8, 9	op2nd 7177	. 2 |- ( 2nd ` <. x , y >. ) = y
11	3, 7, 10	vtocl2g 3270	1 |- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   <.cop 4183   ` cfv 5888   2ndc2nd 7167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fv 5896  df-2nd 7169

This theorem is referenced by:  ot2ndg  7183  ot3rdg  7184  2ndconst  7266  mpt2sn  7268  curry1  7269  xpmapenlem  8127  axdc4lem  9277  pinq  9749  addpipq  9759  mulpipq  9762  ordpipq  9764  swrdval  13417  ruclem1  14960  eucalg  15300  qnumdenbi  15452  setsstruct  15898  comffval  16359  oppccofval  16376  funcf2  16528  cofuval2  16547  resfval2  16553  resf2nd  16555  funcres  16556  isnat  16607  fucco  16622  homacd  16691  setcco  16733  catcco  16751  estrcco  16770  xpcco  16823  xpchom2  16826  xpcco2  16827  evlf2  16858  curfval  16863  curf1cl  16868  uncf1  16876  uncf2  16877  hof2fval  16895  yonedalem21  16913  yonedalem22  16918  mvmulfval  20348  imasdsf1olem  22178  ovolicc1  23284  ioombl1lem3  23328  ioombl1lem4  23329  brcgr  25780  opiedgfv  25887  br2ndeqg  31673  fvtransport  32139  bj-elid3  33087  bj-finsumval0  33147  poimirlem17  33426  poimirlem24  33433  poimirlem27  33436  dvhopvadd  36382  dvhopvsca  36391  dvhopaddN  36403  dvhopspN  36404  etransclem44  40495  uspgrsprfo  41756  rngccoALTV  41988  ringccoALTV  42051  lmod1zr  42282