MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xp2nd Structured version   Unicode version

Theorem xp2nd 6612
Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
xp2nd  |-  ( A  e.  ( B  X.  C )  ->  ( 2nd `  A )  e.  C )

Proof of Theorem xp2nd
Dummy variables  b 
c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 4862 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 2980 . . . . . . 7  |-  b  e. 
_V
3 vex 2980 . . . . . . 7  |-  c  e. 
_V
42, 3op2ndd 6593 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 2nd `  A
)  =  c )
54eleq1d 2509 . . . . 5  |-  ( A  =  <. b ,  c
>.  ->  ( ( 2nd `  A )  e.  C  <->  c  e.  C ) )
65biimpar 485 . . . 4  |-  ( ( A  =  <. b ,  c >.  /\  c  e.  C )  ->  ( 2nd `  A )  e.  C )
76adantrl 715 . . 3  |-  ( ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 2nd `  A )  e.  C
)
87exlimivv 1689 . 2  |-  ( E. b E. c ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 2nd `  A )  e.  C
)
91, 8sylbi 195 1  |-  ( A  e.  ( B  X.  C )  ->  ( 2nd `  A )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   <.cop 3888    X. cxp 4843   ` cfv 5423   2ndc2nd 6581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5386  df-fun 5425  df-fv 5431  df-2nd 6583
This theorem is referenced by:  offval22  6657  disjen  7473  xpf1o  7478  xpmapenlem  7483  mapunen  7485  r0weon  8184  infxpenlem  8185  fseqdom  8201  axcc2lem  8610  iunfo  8708  iundom2g  8709  enqbreq2  9094  nqereu  9103  addpqf  9118  mulpqf  9120  adderpqlem  9128  mulerpqlem  9129  addassnq  9132  mulassnq  9133  distrnq  9135  mulidnq  9137  recmulnq  9138  ltsonq  9143  lterpq  9144  ltanq  9145  ltmnq  9146  ltexnq  9149  archnq  9154  elreal2  9304  cnref1o  10991  fsumcom2  13246  ruclem6  13522  ruclem8  13524  ruclem9  13525  ruclem10  13526  ruclem12  13528  eucalgval  13762  eucalginv  13764  eucalglt  13765  eucalgcvga  13766  eucalg  13767  xpsff1o  14511  comfffval2  14645  comfeq  14650  idfucl  14796  funcpropd  14815  fucpropd  14892  xpccatid  15003  1stfcl  15012  2ndfcl  15013  xpcpropd  15023  hofcl  15074  hofpropd  15082  yonedalem3  15095  lsmhash  16207  gsum2dlem2  16467  gsum2dOLD  16469  dprd2da  16546  evlslem4OLD  17595  evlslem4  17596  mdetunilem9  18431  tx1cn  19187  txdis  19210  txlly  19214  txnlly  19215  txhaus  19225  txkgen  19230  txcon  19267  txhmeo  19381  ptuncnv  19385  ptunhmeo  19386  xkohmeo  19393  utop2nei  19830  utop3cls  19831  imasdsf1olem  19953  cnheiborlem  20531  caubl  20823  caublcls  20824  bcthlem2  20841  bcthlem4  20843  bcthlem5  20844  ovolficcss  20958  ovoliunlem1  20990  ovoliunlem2  20991  ovolicc2lem1  21005  ovolicc2lem2  21006  ovolicc2lem3  21007  ovolicc2lem4  21008  ovolicc2lem5  21009  dyadmbl  21085  fsumvma  22557  disjxpin  25935  cnre2csqima  26346  tpr2rico  26347  1stmbfm  26680  dya2iocnrect  26701  sibfof  26731  fprodcom2  27500  finixpnum  28419  heicant  28431  mblfinlem1  28433  mblfinlem2  28434  ftc2nc  28481  heiborlem8  28722  rmxypairf1o  29257  frmy  29260  dvhfvadd  34741  dvhvaddcl  34745  dvhvaddcomN  34746  dvhvaddass  34747  dvhvscacl  34753  dvhgrp  34757  dvhlveclem  34758  dibelval2nd  34802  dicelval2nd  34839
  Copyright terms: Public domain W3C validator