Theorem xp2nd 8007

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 5675	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3461	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3461	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7985	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2850	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 482	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 728	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1955	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ⟨cop 4591   × cxp 5650  ‘cfv 6525  2^nd c2nd 7973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fv 6533  df-2nd 7975

This theorem is referenced by:  offval22  8071  mpof1o2d  8109  fimaproj  8119  disjen  9110  xpf1o  9115  xpmapenlem  9120  mapunen  9122  djur  9893  r0weon  9984  infxpenlem  9985  fseqdom  9998  axcc2lem  10408  iunfo  10511  iundom2g  10512  enqbreq2  10893  nqereu  10902  addpqf  10917  mulpqf  10919  adderpqlem  10927  mulerpqlem  10928  addassnq  10931  mulassnq  10932  distrnq  10934  mulidnq  10936  recmulnq  10937  ltsonq  10942  lterpq  10943  ltanq  10944  ltmnq  10945  ltexnq  10948  archnq  10953  elreal2  11105  cnref1o  13000  fsumcom2  15815  fprodcom2  16028  ruclem6  16281  ruclem8  16283  ruclem9  16284  ruclem10  16285  ruclem12  16287  eucalgval  16630  eucalginv  16632  eucalglt  16633  eucalgcvga  16634  eucalg  16635  xpsff1o  17611  comfffval2  17747  comfeq  17752  idfucl  17928  funcpropd  17949  fucpropd  18027  xpccatid  18234  1stfcl  18243  2ndfcl  18244  xpcpropd  18254  hofcl  18305  hofpropd  18313  yonedalem3  18326  lsmhash  19766  gsum2dlem2  20032  dprd2da  20105  evlslem4  22187  mdetunilem9  22738  tx1cn  23727  txdis  23750  txlly  23754  txnlly  23755  txhaus  23765  txkgen  23770  txconn  23807  txhmeo  23921  ptuncnv  23925  ptunhmeo  23926  xkohmeo  23933  utop2nei  24368  utop3cls  24369  imasdsf1olem  24491  cnheiborlem  25074  caubl  25428  caublcls  25429  bcthlem2  25445  bcthlem4  25447  bcthlem5  25448  ovolficcss  25589  ovoliunlem1  25622  ovoliunlem2  25623  ovolicc2lem1  25637  ovolicc2lem2  25638  ovolicc2lem3  25639  ovolicc2lem4  25640  ovolicc2lem5  25641  dyadmbl  25720  fsumvma  27335  opreu2reuALT  32733  disjxpin  32843  2ndimaxp  32903  2ndresdju  32906  fsumiunle  33086  gsummpt2d  33282  gsumwrd2dccatlem  33310  conjga  33403  elrgspnlem2  33476  elrgspnsubrunlem2  33481  erler  33498  rlocaddval  33502  rlocmulval  33503  mplvrpmga  33852  cnre2csqima  34218  tpr2rico  34219  esum2dlem  34399  esumiun  34401  1stmbfm  34567  dya2iocnrect  34588  sibfof  34647  sitgaddlemb  34655  hgt750lemb  34960  satefvfmla0  35781  mvrsfpw  35869  msubff  35893  msubco  35894  msubvrs  35923  elxp8  37877  finixpnum  38116  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem14  38145  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem25  38156  poimirlem26  38157  poimirlem27  38158  poimirlem29  38160  poimirlem31  38162  heicant  38166  mblfinlem1  38168  mblfinlem2  38169  ftc2nc  38213  heiborlem8  38329  dvhfvadd  41727  dvhvaddcl  41731  dvhvaddcomN  41732  dvhvaddass  41733  dvhvscacl  41739  dvhgrp  41743  dvhlveclem  41744  dibelval2nd  41788  dicelval2nd  41825  aks6d1c2p1  42747  aks6d1c3  42752  aks6d1c4  42753  aks6d1c6lem2  42800  aks6d1c6lem4  42802  rmxypairf1o  43500  frmy  43503  cnmetcoval  45777  dvnprodlem1  46518  dvnprodlem2  46519  volicoff  46567  voliooicof  46568  etransclem44  46850  etransclem45  46851  etransclem47  46853  hoissre  47116  hoiprodcl  47119  ovnsubaddlem1  47142  ovnhoilem2  47174  hoicoto2  47177  ovncvr2  47183  opnvonmbllem2  47205  ovolval2lem  47215  ovolval3  47219  ovolval4lem1  47221  ovolval4lem2  47222  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229  smfpimbor1lem1  47370  2arymaptf  49283  rrx2xpref1o  49349  elxpcbasex2ALT  49880  swapf2f1oa  49906  swapfida  49909  fuco2eld2  49943  fucoco2  49987  pgindlem  50344