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

Theorem xp2nd 6826
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 5022 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 3121 . . . . . . 7  |-  b  e. 
_V
3 vex 3121 . . . . . . 7  |-  c  e. 
_V
42, 3op2ndd 6806 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 2nd `  A
)  =  c )
54eleq1d 2536 . . . . 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 1699 . 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 1379   E.wex 1596    e. wcel 1767   <.cop 4039    X. cxp 5003   ` cfv 5594   2ndc2nd 6794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-iota 5557  df-fun 5596  df-fv 5602  df-2nd 6796
This theorem is referenced by:  offval22  6874  disjen  7686  xpf1o  7691  xpmapenlem  7696  mapunen  7698  r0weon  8402  infxpenlem  8403  fseqdom  8419  axcc2lem  8828  iunfo  8926  iundom2g  8927  enqbreq2  9310  nqereu  9319  addpqf  9334  mulpqf  9336  adderpqlem  9344  mulerpqlem  9345  addassnq  9348  mulassnq  9349  distrnq  9351  mulidnq  9353  recmulnq  9354  ltsonq  9359  lterpq  9360  ltanq  9361  ltmnq  9362  ltexnq  9365  archnq  9370  elreal2  9521  cnref1o  11227  fsumcom2  13569  ruclem6  13846  ruclem8  13848  ruclem9  13849  ruclem10  13850  ruclem12  13852  eucalgval  14087  eucalginv  14089  eucalglt  14090  eucalgcvga  14091  eucalg  14092  xpsff1o  14840  comfffval2  14974  comfeq  14979  idfucl  15125  funcpropd  15144  fucpropd  15221  xpccatid  15332  1stfcl  15341  2ndfcl  15342  xpcpropd  15352  hofcl  15403  hofpropd  15411  yonedalem3  15424  lsmhash  16596  gsum2dlem2  16871  gsum2dOLD  16873  dprd2da  16963  evlslem4OLD  18043  evlslem4  18044  mdetunilem9  18991  tx1cn  19978  txdis  20001  txlly  20005  txnlly  20006  txhaus  20016  txkgen  20021  txcon  20058  txhmeo  20172  ptuncnv  20176  ptunhmeo  20177  xkohmeo  20184  utop2nei  20621  utop3cls  20622  imasdsf1olem  20744  cnheiborlem  21322  caubl  21614  caublcls  21615  bcthlem2  21632  bcthlem4  21634  bcthlem5  21635  ovolficcss  21749  ovoliunlem1  21781  ovoliunlem2  21782  ovolicc2lem1  21796  ovolicc2lem2  21797  ovolicc2lem3  21798  ovolicc2lem4  21799  ovolicc2lem5  21800  dyadmbl  21877  fsumvma  23354  disjxpin  27270  fimaproj  27661  cnre2csqima  27718  tpr2rico  27719  1stmbfm  28056  dya2iocnrect  28077  sibfof  28107  mvrsfpw  28691  msubff  28715  msubco  28716  msubvrs  28745  fprodcom2  29041  finixpnum  29965  heicant  29976  mblfinlem1  29978  mblfinlem2  29979  ftc2nc  30026  heiborlem8  30241  rmxypairf1o  30775  frmy  30778  dvhfvadd  36289  dvhvaddcl  36293  dvhvaddcomN  36294  dvhvaddass  36295  dvhvscacl  36301  dvhgrp  36305  dvhlveclem  36306  dibelval2nd  36350  dicelval2nd  36387
  Copyright terms: Public domain W3C validator