Theorem xp2nd 7966

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 5645	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3434	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3434	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7944	. . . . . 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 4574   × cxp 5620  ‘cfv 6490  2^nd c2nd 7932

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 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-2nd 7934

This theorem is referenced by:  offval22  8029  fimaproj  8076  disjen  9063  xpf1o  9068  xpmapenlem  9073  mapunen  9075  djur  9832  r0weon  9923  infxpenlem  9924  fseqdom  9937  axcc2lem  10347  iunfo  10450  iundom2g  10451  enqbreq2  10832  nqereu  10841  addpqf  10856  mulpqf  10858  adderpqlem  10866  mulerpqlem  10867  addassnq  10870  mulassnq  10871  distrnq  10873  mulidnq  10875  recmulnq  10876  ltsonq  10881  lterpq  10882  ltanq  10883  ltmnq  10884  ltexnq  10887  archnq  10892  elreal2  11044  cnref1o  12899  fsumcom2  15698  fprodcom2  15908  ruclem6  16161  ruclem8  16163  ruclem9  16164  ruclem10  16165  ruclem12  16167  eucalgval  16510  eucalginv  16512  eucalglt  16513  eucalgcvga  16514  eucalg  16515  xpsff1o  17489  comfffval2  17625  comfeq  17630  idfucl  17806  funcpropd  17827  fucpropd  17905  xpccatid  18112  1stfcl  18121  2ndfcl  18122  xpcpropd  18132  hofcl  18183  hofpropd  18191  yonedalem3  18204  lsmhash  19638  gsum2dlem2  19904  dprd2da  19977  evlslem4  22032  mdetunilem9  22563  tx1cn  23552  txdis  23575  txlly  23579  txnlly  23580  txhaus  23590  txkgen  23595  txconn  23632  txhmeo  23746  ptuncnv  23750  ptunhmeo  23751  xkohmeo  23758  utop2nei  24193  utop3cls  24194  imasdsf1olem  24316  cnheiborlem  24899  caubl  25253  caublcls  25254  bcthlem2  25270  bcthlem4  25272  bcthlem5  25273  ovolficcss  25414  ovoliunlem1  25447  ovoliunlem2  25448  ovolicc2lem1  25462  ovolicc2lem2  25463  ovolicc2lem3  25464  ovolicc2lem4  25465  ovolicc2lem5  25466  dyadmbl  25545  fsumvma  27164  opreu2reuALT  32535  disjxpin  32647  2ndimaxp  32708  2ndresdju  32711  fsumiunle  32893  gsummpt2d  33115  gsumwrd2dccatlem  33143  conjga  33236  elrgspnlem2  33309  elrgspnsubrunlem2  33314  erler  33331  rlocaddval  33334  rlocmulval  33335  mplvrpmga  33694  cnre2csqima  34061  tpr2rico  34062  esum2dlem  34242  esumiun  34244  1stmbfm  34410  dya2iocnrect  34431  sibfof  34490  sitgaddlemb  34498  hgt750lemb  34806  satefvfmla0  35606  mvrsfpw  35694  msubff  35718  msubco  35719  msubvrs  35748  elxp8  37683  finixpnum  37917  poimirlem4  37936  poimirlem5  37937  poimirlem6  37938  poimirlem7  37939  poimirlem8  37940  poimirlem9  37941  poimirlem10  37942  poimirlem11  37943  poimirlem12  37944  poimirlem13  37945  poimirlem14  37946  poimirlem15  37947  poimirlem16  37948  poimirlem17  37949  poimirlem18  37950  poimirlem19  37951  poimirlem20  37952  poimirlem21  37953  poimirlem22  37954  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  poimirlem29  37961  poimirlem31  37963  heicant  37967  mblfinlem1  37969  mblfinlem2  37970  ftc2nc  38014  heiborlem8  38130  dvhfvadd  41528  dvhvaddcl  41532  dvhvaddcomN  41533  dvhvaddass  41534  dvhvscacl  41540  dvhgrp  41544  dvhlveclem  41545  dibelval2nd  41589  dicelval2nd  41626  aks6d1c2p1  42549  aks6d1c3  42554  aks6d1c4  42555  aks6d1c6lem2  42602  aks6d1c6lem4  42604  f1o2d2  42666  rmxypairf1o  43342  frmy  43345  cnmetcoval  45634  dvnprodlem1  46378  dvnprodlem2  46379  volicoff  46427  voliooicof  46428  etransclem44  46710  etransclem45  46711  etransclem47  46713  hoissre  46976  hoiprodcl  46979  ovnsubaddlem1  47002  ovnhoilem2  47034  hoicoto2  47037  ovncvr2  47043  opnvonmbllem2  47065  ovolval2lem  47075  ovolval3  47079  ovolval4lem1  47081  ovolval4lem2  47082  ovolval5lem2  47085  ovnovollem1  47088  ovnovollem2  47089  smfpimbor1lem1  47230  2arymaptf  49086  rrx2xpref1o  49152  elxpcbasex2ALT  49684  swapf2f1oa  49710  swapfida  49713  fuco2eld2  49747  fucoco2  49791  pgindlem  50148