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

Theorem xp2nd 7151
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 5096 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)))
2 vex 3192 . . . . . . 7 𝑏 ∈ V
3 vex 3192 . . . . . . 7 𝑐 ∈ V
42, 3op2ndd 7131 . . . . . 6 (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd𝐴) = 𝑐)
54eleq1d 2683 . . . . 5 (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd𝐴) ∈ 𝐶𝑐𝐶))
65biimpar 502 . . . 4 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐𝐶) → (2nd𝐴) ∈ 𝐶)
76adantrl 751 . . 3 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
87exlimivv 1857 . 2 (∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (2nd𝐴) ∈ 𝐶)
91, 8sylbi 207 1 (𝐴 ∈ (𝐵 × 𝐶) → (2nd𝐴) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wex 1701  wcel 1987  cop 4159   × cxp 5077  cfv 5852  2nd c2nd 7119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5815  df-fun 5854  df-fv 5860  df-2nd 7121
This theorem is referenced by:  offval22  7205  disjen  8069  xpf1o  8074  xpmapenlem  8079  mapunen  8081  r0weon  8787  infxpenlem  8788  fseqdom  8801  axcc2lem  9210  iunfo  9313  iundom2g  9314  enqbreq2  9694  nqereu  9703  addpqf  9718  mulpqf  9720  adderpqlem  9728  mulerpqlem  9729  addassnq  9732  mulassnq  9733  distrnq  9735  mulidnq  9737  recmulnq  9738  ltsonq  9743  lterpq  9744  ltanq  9745  ltmnq  9746  ltexnq  9749  archnq  9754  elreal2  9905  cnref1o  11779  fsumcom2  14444  fsumcom2OLD  14445  fprodcom2  14650  fprodcom2OLD  14651  ruclem6  14900  ruclem8  14902  ruclem9  14903  ruclem10  14904  ruclem12  14906  eucalgval  15230  eucalginv  15232  eucalglt  15233  eucalgcvga  15234  eucalg  15235  xpsff1o  16160  comfffval2  16293  comfeq  16298  idfucl  16473  funcpropd  16492  fucpropd  16569  xpccatid  16760  1stfcl  16769  2ndfcl  16770  xpcpropd  16780  hofcl  16831  hofpropd  16839  yonedalem3  16852  lsmhash  18050  gsum2dlem2  18302  dprd2da  18373  evlslem4  19440  mdetunilem9  20358  tx1cn  21335  txdis  21358  txlly  21362  txnlly  21363  txhaus  21373  txkgen  21378  txconn  21415  txhmeo  21529  ptuncnv  21533  ptunhmeo  21534  xkohmeo  21541  utop2nei  21977  utop3cls  21978  imasdsf1olem  22101  cnheiborlem  22676  caubl  23029  caublcls  23030  bcthlem2  23045  bcthlem4  23047  bcthlem5  23048  ovolficcss  23161  ovoliunlem1  23193  ovoliunlem2  23194  ovolicc2lem1  23208  ovolicc2lem2  23209  ovolicc2lem3  23210  ovolicc2lem4  23211  ovolicc2lem5  23212  dyadmbl  23291  fsumvma  24855  disjxpin  29269  gsummpt2d  29590  fimaproj  29706  cnre2csqima  29763  tpr2rico  29764  esum2dlem  29959  esumiun  29961  1stmbfm  30127  dya2iocnrect  30148  sibfof  30207  sitgaddlemb  30215  mvrsfpw  31146  msubff  31170  msubco  31171  msubvrs  31200  elxp8  32886  finixpnum  33061  poimirlem4  33080  poimirlem5  33081  poimirlem6  33082  poimirlem7  33083  poimirlem8  33084  poimirlem9  33085  poimirlem10  33086  poimirlem11  33087  poimirlem12  33088  poimirlem13  33089  poimirlem14  33090  poimirlem15  33091  poimirlem16  33092  poimirlem17  33093  poimirlem18  33094  poimirlem19  33095  poimirlem20  33096  poimirlem21  33097  poimirlem22  33098  poimirlem25  33101  poimirlem26  33102  poimirlem27  33103  poimirlem29  33105  poimirlem31  33107  heicant  33111  mblfinlem1  33113  mblfinlem2  33114  ftc2nc  33161  heiborlem8  33284  dvhfvadd  35895  dvhvaddcl  35899  dvhvaddcomN  35900  dvhvaddass  35901  dvhvscacl  35907  dvhgrp  35911  dvhlveclem  35912  dibelval2nd  35956  dicelval2nd  35993  rmxypairf1o  36991  frmy  36994  cnmetcoval  38899  dvnprodlem1  39494  dvnprodlem2  39495  volicoff  39545  voliooicof  39546  etransclem44  39828  etransclem45  39829  etransclem47  39831  hoissre  40091  hoiprodcl  40094  ovnsubaddlem1  40117  ovnhoilem2  40149  hoicoto2  40152  ovncvr2  40158  opnvonmbllem2  40180  ovolval2lem  40190  ovolval3  40194  ovolval4lem1  40196  ovolval4lem2  40197  ovolval5lem2  40200  ovnovollem1  40203  ovnovollem2  40204  smfpimbor1lem1  40338
  Copyright terms: Public domain W3C validator