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

Theorem xp2nd 7184
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 5121 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)))
2 vex 3198 . . . . . . 7 𝑏 ∈ V
3 vex 3198 . . . . . . 7 𝑐 ∈ V
42, 3op2ndd 7164 . . . . . 6 (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd𝐴) = 𝑐)
54eleq1d 2684 . . . . 5 (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd𝐴) ∈ 𝐶𝑐𝐶))
65biimpar 502 . . . 4 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐𝐶) → (2nd𝐴) ∈ 𝐶)
76adantrl 751 . . 3 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
87exlimivv 1858 . 2 (∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
91, 8sylbi 207 1 (𝐴 ∈ (𝐵 × 𝐶) → (2nd𝐴) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wex 1702  wcel 1988  cop 4174   × cxp 5102  cfv 5876  2nd c2nd 7152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-iota 5839  df-fun 5878  df-fv 5884  df-2nd 7154
This theorem is referenced by:  offval22  7238  disjen  8102  xpf1o  8107  xpmapenlem  8112  mapunen  8114  r0weon  8820  infxpenlem  8821  fseqdom  8834  axcc2lem  9243  iunfo  9346  iundom2g  9347  enqbreq2  9727  nqereu  9736  addpqf  9751  mulpqf  9753  adderpqlem  9761  mulerpqlem  9762  addassnq  9765  mulassnq  9766  distrnq  9768  mulidnq  9770  recmulnq  9771  ltsonq  9776  lterpq  9777  ltanq  9778  ltmnq  9779  ltexnq  9782  archnq  9787  elreal2  9938  cnref1o  11812  fsumcom2  14486  fsumcom2OLD  14487  fprodcom2  14695  fprodcom2OLD  14696  ruclem6  14945  ruclem8  14947  ruclem9  14948  ruclem10  14949  ruclem12  14951  eucalgval  15276  eucalginv  15278  eucalglt  15279  eucalgcvga  15280  eucalg  15281  xpsff1o  16209  comfffval2  16342  comfeq  16347  idfucl  16522  funcpropd  16541  fucpropd  16618  xpccatid  16809  1stfcl  16818  2ndfcl  16819  xpcpropd  16829  hofcl  16880  hofpropd  16888  yonedalem3  16901  lsmhash  18099  gsum2dlem2  18351  dprd2da  18422  evlslem4  19489  mdetunilem9  20407  tx1cn  21393  txdis  21416  txlly  21420  txnlly  21421  txhaus  21431  txkgen  21436  txconn  21473  txhmeo  21587  ptuncnv  21591  ptunhmeo  21592  xkohmeo  21599  utop2nei  22035  utop3cls  22036  imasdsf1olem  22159  cnheiborlem  22734  caubl  23087  caublcls  23088  bcthlem2  23103  bcthlem4  23105  bcthlem5  23106  ovolficcss  23219  ovoliunlem1  23251  ovoliunlem2  23252  ovolicc2lem1  23266  ovolicc2lem2  23267  ovolicc2lem3  23268  ovolicc2lem4  23269  ovolicc2lem5  23270  dyadmbl  23349  fsumvma  24919  disjxpin  29373  fsumiunle  29549  gsummpt2d  29755  fimaproj  29874  cnre2csqima  29931  tpr2rico  29932  esum2dlem  30128  esumiun  30130  1stmbfm  30296  dya2iocnrect  30317  sibfof  30376  sitgaddlemb  30384  hgt750lemb  30708  mvrsfpw  31377  msubff  31401  msubco  31402  msubvrs  31431  elxp8  33190  finixpnum  33365  poimirlem4  33384  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem9  33389  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem13  33393  poimirlem14  33394  poimirlem15  33395  poimirlem16  33396  poimirlem17  33397  poimirlem18  33398  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  poimirlem31  33411  heicant  33415  mblfinlem1  33417  mblfinlem2  33418  ftc2nc  33465  heiborlem8  33588  dvhfvadd  36199  dvhvaddcl  36203  dvhvaddcomN  36204  dvhvaddass  36205  dvhvscacl  36211  dvhgrp  36215  dvhlveclem  36216  dibelval2nd  36260  dicelval2nd  36297  rmxypairf1o  37295  frmy  37298  cnmetcoval  39210  dvnprodlem1  39924  dvnprodlem2  39925  volicoff  39975  voliooicof  39976  etransclem44  40258  etransclem45  40259  etransclem47  40261  hoissre  40521  hoiprodcl  40524  ovnsubaddlem1  40547  ovnhoilem2  40579  hoicoto2  40582  ovncvr2  40588  opnvonmbllem2  40610  ovolval2lem  40620  ovolval3  40624  ovolval4lem1  40626  ovolval4lem2  40627  ovolval5lem2  40630  ovnovollem1  40633  ovnovollem2  40634  smfpimbor1lem1  40768
  Copyright terms: Public domain W3C validator