Theorem xp2nd 7960

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 5642	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3440	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3440	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7938	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2816	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 716	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1933	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ⟨cop 4581   × cxp 5617  ‘cfv 6487  2^nd c2nd 7926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6443  df-fun 6489  df-fv 6495  df-2nd 7928

This theorem is referenced by:  offval22  8024  fimaproj  8071  disjen  9053  xpf1o  9058  xpmapenlem  9063  mapunen  9065  djur  9818  r0weon  9909  infxpenlem  9910  fseqdom  9923  axcc2lem  10333  iunfo  10436  iundom2g  10437  enqbreq2  10817  nqereu  10826  addpqf  10841  mulpqf  10843  adderpqlem  10851  mulerpqlem  10852  addassnq  10855  mulassnq  10856  distrnq  10858  mulidnq  10860  recmulnq  10861  ltsonq  10866  lterpq  10867  ltanq  10868  ltmnq  10869  ltexnq  10872  archnq  10877  elreal2  11029  cnref1o  12889  fsumcom2  15687  fprodcom2  15897  ruclem6  16150  ruclem8  16152  ruclem9  16153  ruclem10  16154  ruclem12  16156  eucalgval  16499  eucalginv  16501  eucalglt  16502  eucalgcvga  16503  eucalg  16504  xpsff1o  17477  comfffval2  17613  comfeq  17618  idfucl  17794  funcpropd  17815  fucpropd  17893  xpccatid  18100  1stfcl  18109  2ndfcl  18110  xpcpropd  18120  hofcl  18171  hofpropd  18179  yonedalem3  18192  lsmhash  19623  gsum2dlem2  19889  dprd2da  19962  evlslem4  22017  mdetunilem9  22541  tx1cn  23530  txdis  23553  txlly  23557  txnlly  23558  txhaus  23568  txkgen  23573  txconn  23610  txhmeo  23724  ptuncnv  23728  ptunhmeo  23729  xkohmeo  23736  utop2nei  24171  utop3cls  24172  imasdsf1olem  24294  cnheiborlem  24886  caubl  25241  caublcls  25242  bcthlem2  25258  bcthlem4  25260  bcthlem5  25261  ovolficcss  25403  ovoliunlem1  25436  ovoliunlem2  25437  ovolicc2lem1  25451  ovolicc2lem2  25452  ovolicc2lem3  25453  ovolicc2lem4  25454  ovolicc2lem5  25455  dyadmbl  25534  fsumvma  27157  opreu2reuALT  32463  disjxpin  32575  2ndimaxp  32635  2ndresdju  32638  fsumiunle  32819  gsummpt2d  33036  gsumwrd2dccatlem  33053  conjga  33146  elrgspnlem2  33217  elrgspnsubrunlem2  33222  erler  33239  rlocaddval  33242  rlocmulval  33243  mplvrpmga  33582  cnre2csqima  33931  tpr2rico  33932  esum2dlem  34112  esumiun  34114  1stmbfm  34280  dya2iocnrect  34301  sibfof  34360  sitgaddlemb  34368  hgt750lemb  34676  satefvfmla0  35469  mvrsfpw  35557  msubff  35581  msubco  35582  msubvrs  35611  elxp8  37422  finixpnum  37651  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem29  37695  poimirlem31  37697  heicant  37701  mblfinlem1  37703  mblfinlem2  37704  ftc2nc  37748  heiborlem8  37864  dvhfvadd  41196  dvhvaddcl  41200  dvhvaddcomN  41201  dvhvaddass  41202  dvhvscacl  41208  dvhgrp  41212  dvhlveclem  41213  dibelval2nd  41257  dicelval2nd  41294  aks6d1c2p1  42217  aks6d1c3  42222  aks6d1c4  42223  aks6d1c6lem2  42270  aks6d1c6lem4  42272  f1o2d2  42332  rmxypairf1o  43009  frmy  43012  cnmetcoval  45304  dvnprodlem1  46049  dvnprodlem2  46050  volicoff  46098  voliooicof  46099  etransclem44  46381  etransclem45  46382  etransclem47  46384  hoissre  46647  hoiprodcl  46650  ovnsubaddlem1  46673  ovnhoilem2  46705  hoicoto2  46708  ovncvr2  46714  opnvonmbllem2  46736  ovolval2lem  46746  ovolval3  46750  ovolval4lem1  46752  ovolval4lem2  46753  ovolval5lem2  46756  ovnovollem1  46759  ovnovollem2  46760  smfpimbor1lem1  46901  2arymaptf  48758  rrx2xpref1o  48824  elxpcbasex2ALT  49357  swapf2f1oa  49383  swapfida  49386  fuco2eld2  49420  fucoco2  49464  pgindlem  49821