Theorem xp2nd 7968

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.

Step	Hyp	Ref	Expression
1		elxp 5648	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3445	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3445	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7946	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2822	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 717	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1934	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4587   × cxp 5623  ‘cfv 6493  2^nd c2nd 7934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fv 6501  df-2nd 7936

This theorem is referenced by:  offval22  8032  fimaproj  8079  disjen  9066  xpf1o  9071  xpmapenlem  9076  mapunen  9078  djur  9835  r0weon  9926  infxpenlem  9927  fseqdom  9940  axcc2lem  10350  iunfo  10453  iundom2g  10454  enqbreq2  10835  nqereu  10844  addpqf  10859  mulpqf  10861  adderpqlem  10869  mulerpqlem  10870  addassnq  10873  mulassnq  10874  distrnq  10876  mulidnq  10878  recmulnq  10879  ltsonq  10884  lterpq  10885  ltanq  10886  ltmnq  10887  ltexnq  10890  archnq  10895  elreal2  11047  cnref1o  12902  fsumcom2  15701  fprodcom2  15911  ruclem6  16164  ruclem8  16166  ruclem9  16167  ruclem10  16168  ruclem12  16170  eucalgval  16513  eucalginv  16515  eucalglt  16516  eucalgcvga  16517  eucalg  16518  xpsff1o  17492  comfffval2  17628  comfeq  17633  idfucl  17809  funcpropd  17830  fucpropd  17908  xpccatid  18115  1stfcl  18124  2ndfcl  18125  xpcpropd  18135  hofcl  18186  hofpropd  18194  yonedalem3  18207  lsmhash  19638  gsum2dlem2  19904  dprd2da  19977  evlslem4  22035  mdetunilem9  22568  tx1cn  23557  txdis  23580  txlly  23584  txnlly  23585  txhaus  23595  txkgen  23600  txconn  23637  txhmeo  23751  ptuncnv  23755  ptunhmeo  23756  xkohmeo  23763  utop2nei  24198  utop3cls  24199  imasdsf1olem  24321  cnheiborlem  24913  caubl  25268  caublcls  25269  bcthlem2  25285  bcthlem4  25287  bcthlem5  25288  ovolficcss  25430  ovoliunlem1  25463  ovoliunlem2  25464  ovolicc2lem1  25478  ovolicc2lem2  25479  ovolicc2lem3  25480  ovolicc2lem4  25481  ovolicc2lem5  25482  dyadmbl  25561  fsumvma  27184  opreu2reuALT  32533  disjxpin  32645  2ndimaxp  32706  2ndresdju  32709  fsumiunle  32891  gsummpt2d  33113  gsumwrd2dccatlem  33140  conjga  33233  elrgspnlem2  33306  elrgspnsubrunlem2  33311  erler  33328  rlocaddval  33331  rlocmulval  33332  mplvrpmga  33691  cnre2csqima  34049  tpr2rico  34050  esum2dlem  34230  esumiun  34232  1stmbfm  34398  dya2iocnrect  34419  sibfof  34478  sitgaddlemb  34486  hgt750lemb  34794  satefvfmla0  35593  mvrsfpw  35681  msubff  35705  msubco  35706  msubvrs  35735  elxp8  37547  finixpnum  37777  poimirlem4  37796  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem9  37801  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem13  37805  poimirlem14  37806  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem18  37810  poimirlem19  37811  poimirlem20  37812  poimirlem21  37813  poimirlem22  37814  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimirlem29  37821  poimirlem31  37823  heicant  37827  mblfinlem1  37829  mblfinlem2  37830  ftc2nc  37874  heiborlem8  37990  dvhfvadd  41388  dvhvaddcl  41392  dvhvaddcomN  41393  dvhvaddass  41394  dvhvscacl  41400  dvhgrp  41404  dvhlveclem  41405  dibelval2nd  41449  dicelval2nd  41486  aks6d1c2p1  42409  aks6d1c3  42414  aks6d1c4  42415  aks6d1c6lem2  42462  aks6d1c6lem4  42464  f1o2d2  42526  rmxypairf1o  43189  frmy  43192  cnmetcoval  45482  dvnprodlem1  46226  dvnprodlem2  46227  volicoff  46275  voliooicof  46276  etransclem44  46558  etransclem45  46559  etransclem47  46561  hoissre  46824  hoiprodcl  46827  ovnsubaddlem1  46850  ovnhoilem2  46882  hoicoto2  46885  ovncvr2  46891  opnvonmbllem2  46913  ovolval2lem  46923  ovolval3  46927  ovolval4lem1  46929  ovolval4lem2  46930  ovolval5lem2  46933  ovnovollem1  46936  ovnovollem2  46937  smfpimbor1lem1  47078  2arymaptf  48934  rrx2xpref1o  49000  elxpcbasex2ALT  49532  swapf2f1oa  49558  swapfida  49561  fuco2eld2  49595  fucoco2  49639  pgindlem  49996