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

Theorem xp2nd 7955
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 5657 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)))
2 vex 3450 . . . . . . 7 𝑏 ∈ V
3 vex 3450 . . . . . . 7 𝑐 ∈ V
42, 3op2ndd 7933 . . . . . 6 (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd𝐴) = 𝑐)
54eleq1d 2823 . . . . 5 (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd𝐴) ∈ 𝐶𝑐𝐶))
65biimpar 479 . . . 4 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐𝐶) → (2nd𝐴) ∈ 𝐶)
76adantrl 715 . . 3 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
87exlimivv 1936 . 2 (∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
91, 8sylbi 216 1 (𝐴 ∈ (𝐵 × 𝐶) → (2nd𝐴) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wex 1782  wcel 2107  cop 4593   × cxp 5632  cfv 6497  2nd c2nd 7921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-2nd 7923
This theorem is referenced by:  offval22  8021  fimaproj  8068  disjen  9079  xpf1o  9084  xpmapenlem  9089  mapunen  9091  djur  9856  r0weon  9949  infxpenlem  9950  fseqdom  9963  axcc2lem  10373  iunfo  10476  iundom2g  10477  enqbreq2  10857  nqereu  10866  addpqf  10881  mulpqf  10883  adderpqlem  10891  mulerpqlem  10892  addassnq  10895  mulassnq  10896  distrnq  10898  mulidnq  10900  recmulnq  10901  ltsonq  10906  lterpq  10907  ltanq  10908  ltmnq  10909  ltexnq  10912  archnq  10917  elreal2  11069  cnref1o  12911  fsumcom2  15660  fprodcom2  15868  ruclem6  16118  ruclem8  16120  ruclem9  16121  ruclem10  16122  ruclem12  16124  eucalgval  16459  eucalginv  16461  eucalglt  16462  eucalgcvga  16463  eucalg  16464  xpsff1o  17450  comfffval2  17582  comfeq  17587  idfucl  17768  funcpropd  17788  fucpropd  17867  xpccatid  18077  1stfcl  18086  2ndfcl  18087  xpcpropd  18098  hofcl  18149  hofpropd  18157  yonedalem3  18170  lsmhash  19488  gsum2dlem2  19749  dprd2da  19822  evlslem4  21487  mdetunilem9  21972  tx1cn  22963  txdis  22986  txlly  22990  txnlly  22991  txhaus  23001  txkgen  23006  txconn  23043  txhmeo  23157  ptuncnv  23161  ptunhmeo  23162  xkohmeo  23169  utop2nei  23605  utop3cls  23606  imasdsf1olem  23729  cnheiborlem  24320  caubl  24675  caublcls  24676  bcthlem2  24692  bcthlem4  24694  bcthlem5  24695  ovolficcss  24836  ovoliunlem1  24869  ovoliunlem2  24870  ovolicc2lem1  24884  ovolicc2lem2  24885  ovolicc2lem3  24886  ovolicc2lem4  24887  ovolicc2lem5  24888  dyadmbl  24967  fsumvma  26564  opreu2reuALT  31408  disjxpin  31509  2ndimaxp  31566  2ndresdju  31568  fsumiunle  31728  gsummpt2d  31894  cnre2csqima  32495  tpr2rico  32496  esum2dlem  32694  esumiun  32696  1stmbfm  32863  dya2iocnrect  32884  sibfof  32943  sitgaddlemb  32951  hgt750lemb  33272  satefvfmla0  34015  mvrsfpw  34103  msubff  34127  msubco  34128  msubvrs  34157  elxp8  35845  finixpnum  36066  poimirlem4  36085  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem8  36089  poimirlem9  36090  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem13  36094  poimirlem14  36095  poimirlem15  36096  poimirlem16  36097  poimirlem17  36098  poimirlem18  36099  poimirlem19  36100  poimirlem20  36101  poimirlem21  36102  poimirlem22  36103  poimirlem25  36106  poimirlem26  36107  poimirlem27  36108  poimirlem29  36110  poimirlem31  36112  heicant  36116  mblfinlem1  36118  mblfinlem2  36119  ftc2nc  36163  heiborlem8  36280  dvhfvadd  39557  dvhvaddcl  39561  dvhvaddcomN  39562  dvhvaddass  39563  dvhvscacl  39569  dvhgrp  39573  dvhlveclem  39574  dibelval2nd  39618  dicelval2nd  39655  aks6d1c2p1  40551  rmxypairf1o  41238  frmy  41241  cnmetcoval  43430  dvnprodlem1  44194  dvnprodlem2  44195  volicoff  44243  voliooicof  44244  etransclem44  44526  etransclem45  44527  etransclem47  44529  hoissre  44792  hoiprodcl  44795  ovnsubaddlem1  44818  ovnhoilem2  44850  hoicoto2  44853  ovncvr2  44859  opnvonmbllem2  44881  ovolval2lem  44891  ovolval3  44895  ovolval4lem1  44897  ovolval4lem2  44898  ovolval5lem2  44901  ovnovollem1  44904  ovnovollem2  44905  smfpimbor1lem1  45046  2arymaptf  46745  rrx2xpref1o  46811  pgindlem  47167
  Copyright terms: Public domain W3C validator