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

Theorem xp2nd 6843
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 4856 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 3034 . . . . . . 7  |-  b  e. 
_V
3 vex 3034 . . . . . . 7  |-  c  e. 
_V
42, 3op2ndd 6823 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 2nd `  A
)  =  c )
54eleq1d 2533 . . . . 5  |-  ( A  =  <. b ,  c
>.  ->  ( ( 2nd `  A )  e.  C  <->  c  e.  C ) )
65biimpar 493 . . . 4  |-  ( ( A  =  <. b ,  c >.  /\  c  e.  C )  ->  ( 2nd `  A )  e.  C )
76adantrl 730 . . 3  |-  ( ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 2nd `  A )  e.  C
)
87exlimivv 1786 . 2  |-  ( E. b E. c ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 2nd `  A )  e.  C
)
91, 8sylbi 200 1  |-  ( A  e.  ( B  X.  C )  ->  ( 2nd `  A )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452   E.wex 1671    e. wcel 1904   <.cop 3965    X. cxp 4837   ` cfv 5589   2ndc2nd 6811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-iota 5553  df-fun 5591  df-fv 5597  df-2nd 6813
This theorem is referenced by:  offval22  6891  disjen  7747  xpf1o  7752  xpmapenlem  7757  mapunen  7759  r0weon  8461  infxpenlem  8462  fseqdom  8475  axcc2lem  8884  iunfo  8982  iundom2g  8983  enqbreq2  9363  nqereu  9372  addpqf  9387  mulpqf  9389  adderpqlem  9397  mulerpqlem  9398  addassnq  9401  mulassnq  9402  distrnq  9404  mulidnq  9406  recmulnq  9407  ltsonq  9412  lterpq  9413  ltanq  9414  ltmnq  9415  ltexnq  9418  archnq  9423  elreal2  9574  cnref1o  11320  fsumcom2  13912  fprodcom2  14115  ruclem6  14364  ruclem8  14366  ruclem9  14367  ruclem10  14368  ruclem12  14370  eucalgval  14620  eucalginv  14622  eucalglt  14623  eucalgcvga  14624  eucalg  14625  xpsff1o  15552  comfffval2  15684  comfeq  15689  idfucl  15864  funcpropd  15883  fucpropd  15960  xpccatid  16151  1stfcl  16160  2ndfcl  16161  xpcpropd  16171  hofcl  16222  hofpropd  16230  yonedalem3  16243  lsmhash  17433  gsum2dlem2  17681  dprd2da  17753  evlslem4  18808  mdetunilem9  19722  tx1cn  20701  txdis  20724  txlly  20728  txnlly  20729  txhaus  20739  txkgen  20744  txcon  20781  txhmeo  20895  ptuncnv  20899  ptunhmeo  20900  xkohmeo  20907  utop2nei  21343  utop3cls  21344  imasdsf1olem  21466  cnheiborlem  22060  caubl  22355  caublcls  22356  bcthlem2  22371  bcthlem4  22373  bcthlem5  22374  ovolficcss  22500  ovoliunlem1  22533  ovoliunlem2  22534  ovolicc2lem1  22548  ovolicc2lem2  22549  ovolicc2lem3  22550  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2lem5  22553  dyadmbl  22637  fsumvma  24220  disjxpin  28275  gsummpt2d  28618  fimaproj  28734  cnre2csqima  28791  tpr2rico  28792  esum2dlem  28987  esumiun  28989  1stmbfm  29155  dya2iocnrect  29176  sibfof  29246  sitgaddlemb  29254  mvrsfpw  30216  msubff  30240  msubco  30241  msubvrs  30270  elxp8  31844  finixpnum  31994  poimirlem4  32008  poimirlem5  32009  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem9  32013  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem13  32017  poimirlem14  32018  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem29  32033  poimirlem31  32035  heicant  32039  mblfinlem1  32041  mblfinlem2  32042  ftc2nc  32090  heiborlem8  32214  dvhfvadd  34730  dvhvaddcl  34734  dvhvaddcomN  34735  dvhvaddass  34736  dvhvscacl  34742  dvhgrp  34746  dvhlveclem  34747  dibelval2nd  34791  dicelval2nd  34828  rmxypairf1o  35830  frmy  35833  cnmetcoval  37554  dvnprodlem1  37918  dvnprodlem2  37919  volicoff  37970  voliooicof  37971  etransclem44  38255  etransclem45  38256  etransclem47  38258  hoissre  38484  hoiprodcl  38487  ovnsubaddlem1  38510  ovnhoilem2  38542  hoicoto2  38545  ovncvr2  38551  opnvonmbllem2  38573  ovolval2lem  38583  ovolval3  38587  ovolval4lem1  38589  ovolval4lem2  38590  ovolval5lem2  38593  ovnovollem1  38596  ovnovollem2  38597
  Copyright terms: Public domain W3C validator