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

Theorem xp2nd 7366
Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
xp2nd (𝐴 ∈ (𝐵 × 𝐶) → (2nd𝐴) ∈ 𝐶)

Proof of Theorem xp2nd
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 5288 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)))
2 vex 3343 . . . . . . 7 𝑏 ∈ V
3 vex 3343 . . . . . . 7 𝑐 ∈ V
42, 3op2ndd 7344 . . . . . 6 (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd𝐴) = 𝑐)
54eleq1d 2824 . . . . 5 (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd𝐴) ∈ 𝐶𝑐𝐶))
65biimpar 503 . . . 4 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐𝐶) → (2nd𝐴) ∈ 𝐶)
76adantrl 754 . . 3 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
87exlimivv 2009 . 2 (∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
91, 8sylbi 207 1 (𝐴 ∈ (𝐵 × 𝐶) → (2nd𝐴) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wex 1853  wcel 2139  cop 4327   × cxp 5264  cfv 6049  2nd c2nd 7332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fv 6057  df-2nd 7334
This theorem is referenced by:  offval22  7421  disjen  8282  xpf1o  8287  xpmapenlem  8292  mapunen  8294  djulf1o  8946  djurf1o  8947  djur  8949  r0weon  9025  infxpenlem  9026  fseqdom  9039  axcc2lem  9450  iunfo  9553  iundom2g  9554  enqbreq2  9934  nqereu  9943  addpqf  9958  mulpqf  9960  adderpqlem  9968  mulerpqlem  9969  addassnq  9972  mulassnq  9973  distrnq  9975  mulidnq  9977  recmulnq  9978  ltsonq  9983  lterpq  9984  ltanq  9985  ltmnq  9986  ltexnq  9989  archnq  9994  elreal2  10145  cnref1o  12020  fsumcom2  14704  fsumcom2OLD  14705  fprodcom2  14913  fprodcom2OLD  14914  ruclem6  15163  ruclem8  15165  ruclem9  15166  ruclem10  15167  ruclem12  15169  eucalgval  15497  eucalginv  15499  eucalglt  15500  eucalgcvga  15501  eucalg  15502  xpsff1o  16430  comfffval2  16562  comfeq  16567  idfucl  16742  funcpropd  16761  fucpropd  16838  xpccatid  17029  1stfcl  17038  2ndfcl  17039  xpcpropd  17049  hofcl  17100  hofpropd  17108  yonedalem3  17121  lsmhash  18318  gsum2dlem2  18570  dprd2da  18641  evlslem4  19710  mdetunilem9  20628  tx1cn  21614  txdis  21637  txlly  21641  txnlly  21642  txhaus  21652  txkgen  21657  txconn  21694  txhmeo  21808  ptuncnv  21812  ptunhmeo  21813  xkohmeo  21820  utop2nei  22255  utop3cls  22256  imasdsf1olem  22379  cnheiborlem  22954  caubl  23306  caublcls  23307  bcthlem2  23322  bcthlem4  23324  bcthlem5  23325  ovolficcss  23438  ovoliunlem1  23470  ovoliunlem2  23471  ovolicc2lem1  23485  ovolicc2lem2  23486  ovolicc2lem3  23487  ovolicc2lem4  23488  ovolicc2lem5  23489  dyadmbl  23568  fsumvma  25137  disjxpin  29708  fsumiunle  29884  gsummpt2d  30090  fimaproj  30209  cnre2csqima  30266  tpr2rico  30267  esum2dlem  30463  esumiun  30465  1stmbfm  30631  dya2iocnrect  30652  sibfof  30711  sitgaddlemb  30719  hgt750lemb  31043  mvrsfpw  31710  msubff  31734  msubco  31735  msubvrs  31764  elxp8  33530  finixpnum  33707  poimirlem4  33726  poimirlem5  33727  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem9  33731  poimirlem10  33732  poimirlem11  33733  poimirlem12  33734  poimirlem13  33735  poimirlem14  33736  poimirlem15  33737  poimirlem16  33738  poimirlem17  33739  poimirlem18  33740  poimirlem19  33741  poimirlem20  33742  poimirlem21  33743  poimirlem22  33744  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  poimirlem29  33751  poimirlem31  33753  heicant  33757  mblfinlem1  33759  mblfinlem2  33760  ftc2nc  33807  heiborlem8  33930  dvhfvadd  36882  dvhvaddcl  36886  dvhvaddcomN  36887  dvhvaddass  36888  dvhvscacl  36894  dvhgrp  36898  dvhlveclem  36899  dibelval2nd  36943  dicelval2nd  36980  rmxypairf1o  37978  frmy  37981  cnmetcoval  39893  dvnprodlem1  40664  dvnprodlem2  40665  volicoff  40715  voliooicof  40716  etransclem44  40998  etransclem45  40999  etransclem47  41001  hoissre  41264  hoiprodcl  41267  ovnsubaddlem1  41290  ovnhoilem2  41322  hoicoto2  41325  ovncvr2  41331  opnvonmbllem2  41353  ovolval2lem  41363  ovolval3  41367  ovolval4lem1  41369  ovolval4lem2  41370  ovolval5lem2  41373  ovnovollem1  41376  ovnovollem2  41377  smfpimbor1lem1  41511
  Copyright terms: Public domain W3C validator