Theorem xp2nd 8025

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 5700	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3467	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3467	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 8003	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2810	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 476	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 714	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1927	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ⟨cop 4635   × cxp 5675  ‘cfv 6547  2^nd c2nd 7991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6499  df-fun 6549  df-fv 6555  df-2nd 7993

This theorem is referenced by:  offval22  8091  fimaproj  8138  disjen  9157  xpf1o  9162  xpmapenlem  9167  mapunen  9169  djur  9942  r0weon  10035  infxpenlem  10036  fseqdom  10049  axcc2lem  10459  iunfo  10562  iundom2g  10563  enqbreq2  10943  nqereu  10952  addpqf  10967  mulpqf  10969  adderpqlem  10977  mulerpqlem  10978  addassnq  10981  mulassnq  10982  distrnq  10984  mulidnq  10986  recmulnq  10987  ltsonq  10992  lterpq  10993  ltanq  10994  ltmnq  10995  ltexnq  10998  archnq  11003  elreal2  11155  cnref1o  12999  fsumcom2  15752  fprodcom2  15960  ruclem6  16211  ruclem8  16213  ruclem9  16214  ruclem10  16215  ruclem12  16217  eucalgval  16552  eucalginv  16554  eucalglt  16555  eucalgcvga  16556  eucalg  16557  xpsff1o  17548  comfffval2  17680  comfeq  17685  idfucl  17866  funcpropd  17888  fucpropd  17968  xpccatid  18178  1stfcl  18187  2ndfcl  18188  xpcpropd  18199  hofcl  18250  hofpropd  18258  yonedalem3  18271  lsmhash  19664  gsum2dlem2  19930  dprd2da  20003  evlslem4  22027  mdetunilem9  22552  tx1cn  23543  txdis  23566  txlly  23570  txnlly  23571  txhaus  23581  txkgen  23586  txconn  23623  txhmeo  23737  ptuncnv  23741  ptunhmeo  23742  xkohmeo  23749  utop2nei  24185  utop3cls  24186  imasdsf1olem  24309  cnheiborlem  24910  caubl  25266  caublcls  25267  bcthlem2  25283  bcthlem4  25285  bcthlem5  25286  ovolficcss  25428  ovoliunlem1  25461  ovoliunlem2  25462  ovolicc2lem1  25476  ovolicc2lem2  25477  ovolicc2lem3  25478  ovolicc2lem4  25479  ovolicc2lem5  25480  dyadmbl  25559  fsumvma  27176  opreu2reuALT  32332  disjxpin  32435  2ndimaxp  32490  2ndresdju  32492  fsumiunle  32649  gsummpt2d  32820  erler  33019  rlocaddval  33022  rlocmulval  33023  cnre2csqima  33582  tpr2rico  33583  esum2dlem  33781  esumiun  33783  1stmbfm  33950  dya2iocnrect  33971  sibfof  34030  sitgaddlemb  34038  hgt750lemb  34358  satefvfmla0  35098  mvrsfpw  35186  msubff  35210  msubco  35211  msubvrs  35240  elxp8  36920  finixpnum  37148  poimirlem4  37167  poimirlem5  37168  poimirlem6  37169  poimirlem7  37170  poimirlem8  37171  poimirlem9  37172  poimirlem10  37173  poimirlem11  37174  poimirlem12  37175  poimirlem13  37176  poimirlem14  37177  poimirlem15  37178  poimirlem16  37179  poimirlem17  37180  poimirlem18  37181  poimirlem19  37182  poimirlem20  37183  poimirlem21  37184  poimirlem22  37185  poimirlem25  37188  poimirlem26  37189  poimirlem27  37190  poimirlem29  37192  poimirlem31  37194  heicant  37198  mblfinlem1  37200  mblfinlem2  37201  ftc2nc  37245  heiborlem8  37361  dvhfvadd  40633  dvhvaddcl  40637  dvhvaddcomN  40638  dvhvaddass  40639  dvhvscacl  40645  dvhgrp  40649  dvhlveclem  40650  dibelval2nd  40694  dicelval2nd  40731  aks6d1c2p1  41658  aks6d1c3  41663  aks6d1c4  41664  aks6d1c6lem2  41712  aks6d1c6lem4  41714  f1o2d2  41792  rmxypairf1o  42397  frmy  42400  cnmetcoval  44639  dvnprodlem1  45397  dvnprodlem2  45398  volicoff  45446  voliooicof  45447  etransclem44  45729  etransclem45  45730  etransclem47  45732  hoissre  45995  hoiprodcl  45998  ovnsubaddlem1  46021  ovnhoilem2  46053  hoicoto2  46056  ovncvr2  46062  opnvonmbllem2  46084  ovolval2lem  46094  ovolval3  46098  ovolval4lem1  46100  ovolval4lem2  46101  ovolval5lem2  46104  ovnovollem1  46107  ovnovollem2  46108  smfpimbor1lem1  46249  2arymaptf  47837  rrx2xpref1o  47903  pgindlem  48258