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

Theorem xp2nd 6777
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 4808 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 3020 . . . . . . 7  |-  b  e. 
_V
3 vex 3020 . . . . . . 7  |-  c  e. 
_V
42, 3op2ndd 6757 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 2nd `  A
)  =  c )
54eleq1d 2485 . . . . 5  |-  ( A  =  <. b ,  c
>.  ->  ( ( 2nd `  A )  e.  C  <->  c  e.  C ) )
65biimpar 487 . . . 4  |-  ( ( A  =  <. b ,  c >.  /\  c  e.  C )  ->  ( 2nd `  A )  e.  C )
76adantrl 720 . . 3  |-  ( ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 2nd `  A )  e.  C
)
87exlimivv 1771 . 2  |-  ( E. b E. c ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 2nd `  A )  e.  C
)
91, 8sylbi 198 1  |-  ( A  e.  ( B  X.  C )  ->  ( 2nd `  A )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   E.wex 1657    e. wcel 1872   <.cop 3942    X. cxp 4789   ` cfv 5539   2ndc2nd 6745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-iota 5503  df-fun 5541  df-fv 5547  df-2nd 6747
This theorem is referenced by:  offval22  6825  disjen  7677  xpf1o  7682  xpmapenlem  7687  mapunen  7689  r0weon  8390  infxpenlem  8391  fseqdom  8403  axcc2lem  8812  iunfo  8910  iundom2g  8911  enqbreq2  9291  nqereu  9300  addpqf  9315  mulpqf  9317  adderpqlem  9325  mulerpqlem  9326  addassnq  9329  mulassnq  9330  distrnq  9332  mulidnq  9334  recmulnq  9335  ltsonq  9340  lterpq  9341  ltanq  9342  ltmnq  9343  ltexnq  9346  archnq  9351  elreal2  9502  cnref1o  11243  fsumcom2  13773  fprodcom2  13976  ruclem6  14225  ruclem8  14227  ruclem9  14228  ruclem10  14229  ruclem12  14231  eucalgval  14479  eucalginv  14481  eucalglt  14482  eucalgcvga  14483  eucalg  14484  xpsff1o  15412  comfffval2  15544  comfeq  15549  idfucl  15724  funcpropd  15743  fucpropd  15820  xpccatid  16011  1stfcl  16020  2ndfcl  16021  xpcpropd  16031  hofcl  16082  hofpropd  16090  yonedalem3  16103  lsmhash  17293  gsum2dlem2  17541  dprd2da  17613  evlslem4  18669  mdetunilem9  19582  tx1cn  20561  txdis  20584  txlly  20588  txnlly  20589  txhaus  20599  txkgen  20604  txcon  20641  txhmeo  20755  ptuncnv  20759  ptunhmeo  20760  xkohmeo  20767  utop2nei  21202  utop3cls  21203  imasdsf1olem  21325  cnheiborlem  21919  caubl  22214  caublcls  22215  bcthlem2  22230  bcthlem4  22232  bcthlem5  22233  ovolficcss  22359  ovoliunlem1  22392  ovoliunlem2  22393  ovolicc2lem1  22407  ovolicc2lem2  22408  ovolicc2lem3  22409  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ovolicc2lem5  22412  dyadmbl  22495  fsumvma  24078  disjxpin  28139  gsummpt2d  28490  fimaproj  28607  cnre2csqima  28664  tpr2rico  28665  esum2dlem  28860  esumiun  28862  1stmbfm  29029  dya2iocnrect  29050  sibfof  29120  sitgaddlemb  29128  mvrsfpw  30091  msubff  30115  msubco  30116  msubvrs  30145  elxp8  31681  finixpnum  31837  poimirlem4  31851  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem9  31856  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem13  31860  poimirlem14  31861  poimirlem15  31862  poimirlem16  31863  poimirlem17  31864  poimirlem18  31865  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  poimirlem29  31876  poimirlem31  31878  heicant  31882  mblfinlem1  31884  mblfinlem2  31885  ftc2nc  31933  heiborlem8  32057  dvhfvadd  34571  dvhvaddcl  34575  dvhvaddcomN  34576  dvhvaddass  34577  dvhvscacl  34583  dvhgrp  34587  dvhlveclem  34588  dibelval2nd  34632  dicelval2nd  34669  rmxypairf1o  35672  frmy  35675  dvnprodlem1  37704  dvnprodlem2  37705  etransclem44  38026  etransclem45  38027  etransclem47  38029  hoissre  38213  hoiprodcl  38216  ovnsubaddlem1  38239  ovnhoilem2  38271
  Copyright terms: Public domain W3C validator