Theorem xp2nd 7969

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 7947	. . . . . 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 7935

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 7683

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 7937

This theorem is referenced by:  offval22  8033  fimaproj  8080  disjen  9067  xpf1o  9072  xpmapenlem  9077  mapunen  9079  djur  9836  r0weon  9927  infxpenlem  9928  fseqdom  9941  axcc2lem  10351  iunfo  10454  iundom2g  10455  enqbreq2  10836  nqereu  10845  addpqf  10860  mulpqf  10862  adderpqlem  10870  mulerpqlem  10871  addassnq  10874  mulassnq  10875  distrnq  10877  mulidnq  10879  recmulnq  10880  ltsonq  10885  lterpq  10886  ltanq  10887  ltmnq  10888  ltexnq  10891  archnq  10896  elreal2  11048  cnref1o  12903  fsumcom2  15702  fprodcom2  15912  ruclem6  16165  ruclem8  16167  ruclem9  16168  ruclem10  16169  ruclem12  16171  eucalgval  16514  eucalginv  16516  eucalglt  16517  eucalgcvga  16518  eucalg  16519  xpsff1o  17493  comfffval2  17629  comfeq  17634  idfucl  17810  funcpropd  17831  fucpropd  17909  xpccatid  18116  1stfcl  18125  2ndfcl  18126  xpcpropd  18136  hofcl  18187  hofpropd  18195  yonedalem3  18208  lsmhash  19639  gsum2dlem2  19905  dprd2da  19978  evlslem4  22036  mdetunilem9  22569  tx1cn  23558  txdis  23581  txlly  23585  txnlly  23586  txhaus  23596  txkgen  23601  txconn  23638  txhmeo  23752  ptuncnv  23756  ptunhmeo  23757  xkohmeo  23764  utop2nei  24199  utop3cls  24200  imasdsf1olem  24322  cnheiborlem  24914  caubl  25269  caublcls  25270  bcthlem2  25286  bcthlem4  25288  bcthlem5  25289  ovolficcss  25431  ovoliunlem1  25464  ovoliunlem2  25465  ovolicc2lem1  25479  ovolicc2lem2  25480  ovolicc2lem3  25481  ovolicc2lem4  25482  ovolicc2lem5  25483  dyadmbl  25562  fsumvma  27185  opreu2reuALT  32555  disjxpin  32667  2ndimaxp  32728  2ndresdju  32731  fsumiunle  32913  gsummpt2d  33135  gsumwrd2dccatlem  33163  conjga  33256  elrgspnlem2  33329  elrgspnsubrunlem2  33334  erler  33351  rlocaddval  33354  rlocmulval  33355  mplvrpmga  33714  cnre2csqima  34081  tpr2rico  34082  esum2dlem  34262  esumiun  34264  1stmbfm  34430  dya2iocnrect  34451  sibfof  34510  sitgaddlemb  34518  hgt750lemb  34826  satefvfmla0  35625  mvrsfpw  35713  msubff  35737  msubco  35738  msubvrs  35767  elxp8  37589  finixpnum  37819  poimirlem4  37838  poimirlem5  37839  poimirlem6  37840  poimirlem7  37841  poimirlem8  37842  poimirlem9  37843  poimirlem10  37844  poimirlem11  37845  poimirlem12  37846  poimirlem13  37847  poimirlem14  37848  poimirlem15  37849  poimirlem16  37850  poimirlem17  37851  poimirlem18  37852  poimirlem19  37853  poimirlem20  37854  poimirlem21  37855  poimirlem22  37856  poimirlem25  37859  poimirlem26  37860  poimirlem27  37861  poimirlem29  37863  poimirlem31  37865  heicant  37869  mblfinlem1  37871  mblfinlem2  37872  ftc2nc  37916  heiborlem8  38032  dvhfvadd  41430  dvhvaddcl  41434  dvhvaddcomN  41435  dvhvaddass  41436  dvhvscacl  41442  dvhgrp  41446  dvhlveclem  41447  dibelval2nd  41491  dicelval2nd  41528  aks6d1c2p1  42451  aks6d1c3  42456  aks6d1c4  42457  aks6d1c6lem2  42504  aks6d1c6lem4  42506  f1o2d2  42568  rmxypairf1o  43231  frmy  43234  cnmetcoval  45523  dvnprodlem1  46267  dvnprodlem2  46268  volicoff  46316  voliooicof  46317  etransclem44  46599  etransclem45  46600  etransclem47  46602  hoissre  46865  hoiprodcl  46868  ovnsubaddlem1  46891  ovnhoilem2  46923  hoicoto2  46926  ovncvr2  46932  opnvonmbllem2  46954  ovolval2lem  46964  ovolval3  46968  ovolval4lem1  46970  ovolval4lem2  46971  ovolval5lem2  46974  ovnovollem1  46977  ovnovollem2  46978  smfpimbor1lem1  47119  2arymaptf  48975  rrx2xpref1o  49041  elxpcbasex2ALT  49573  swapf2f1oa  49599  swapfida  49602  fuco2eld2  49636  fucoco2  49680  pgindlem  50037