Theorem xp2nd 8022

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 5682	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3457	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3457	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 8000	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2847	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 483	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 729	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1965	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ⟨cop 4593   × cxp 5657  ‘cfv 6537  2^nd c2nd 7988

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fv 6545  df-2nd 7990

This theorem is used by:  offval22  8088  mpof1o2d  8126  fimaproj  8136  disjen  9135  xpf1o  9140  xpmapenlem  9145  mapunen  9147  djur  9927  r0weon  10018  infxpenlem  10019  fseqdom  10032  axcc2lem  10441  iunfo  10550  iundom2g  10551  enqbreq2  10932  nqereu  10941  addpqf  10956  mulpqf  10958  adderpqlem  10966  mulerpqlem  10967  addassnq  10970  mulassnq  10971  distrnq  10973  mulidnq  10975  recmulnq  10976  ltsonq  10981  lterpq  10982  ltanq  10983  ltmnq  10984  ltexnq  10987  archnq  10992  elreal2  11144  cnref1o  13037  fsumcom2  15862  fprodcom2  16075  ruclem6  16327  ruclem8  16329  ruclem9  16330  ruclem10  16331  ruclem12  16333  eucalgval  16676  eucalginv  16678  eucalglt  16679  eucalgcvga  16680  eucalg  16681  xpsff1o  17657  comfffval2  17793  comfeq  17798  idfucl  17974  funcpropd  17995  fucpropd  18073  xpccatid  18280  1stfcl  18289  2ndfcl  18290  xpcpropd  18300  hofcl  18351  hofpropd  18359  yonedalem3  18372  lsmhash  19833  gsum2dlem2  20099  dprd2da  20172  evlslem4  22293  mdetunilem9  22843  tx1cn  23836  txdis  23859  txlly  23863  txnlly  23864  txhaus  23874  txkgen  23879  txconn  23916  txhmeo  24030  ptuncnv  24034  ptunhmeo  24035  xkohmeo  24042  utop2nei  24477  utop3cls  24478  imasdsf1olem  24600  cnheiborlem  25183  caubl  25537  caublcls  25538  bcthlem2  25554  bcthlem4  25556  bcthlem5  25557  ovolficcss  25698  ovoliunlem1  25731  ovoliunlem2  25732  ovolicc2lem1  25746  ovolicc2lem2  25747  ovolicc2lem3  25748  ovolicc2lem4  25749  ovolicc2lem5  25750  dyadmbl  25829  fsumvma  27447  opreu2reuALT  32938  disjxpin  33048  2ndimaxp  33106  2ndresdju  33109  fsumiunle  33286  gsummpt2d  33476  gsumwrd2dccatlem  33504  conjga  33597  elrgspnlem2  33670  elrgspnsubrunlem2  33675  erler  33692  rlocaddval  33696  rlocmulval  33697  mplvrpmga  34042  cnre2csqima  34408  tpr2rico  34409  esum2dlem  34589  esumiun  34591  1stmbfm  34758  dya2iocnrect  34779  sibfof  34838  sitgaddlemb  34846  hgt750lemb  35151  satefvfmla0  35984  mvrsfpw  36072  msubff  36096  msubco  36097  msubvrs  36126  elxp8  38112  finixpnum  38346  poimirlem4  38360  poimirlem5  38361  poimirlem6  38362  poimirlem7  38363  poimirlem8  38364  poimirlem9  38365  poimirlem10  38366  poimirlem11  38367  poimirlem12  38368  poimirlem13  38369  poimirlem14  38370  poimirlem15  38371  poimirlem16  38372  poimirlem17  38373  poimirlem18  38374  poimirlem19  38375  poimirlem20  38376  poimirlem21  38377  poimirlem22  38378  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem29  38385  poimirlem31  38387  heicant  38391  mblfinlem1  38393  mblfinlem2  38394  ftc2nc  38438  heiborlem8  38555  dvhfvadd  41951  dvhvaddcl  41955  dvhvaddcomN  41956  dvhvaddass  41957  dvhvscacl  41963  dvhgrp  41967  dvhlveclem  41968  dibelval2nd  42012  dicelval2nd  42049  aks6d1c2p1  42971  aks6d1c3  42976  aks6d1c4  42977  aks6d1c6lem2  43024  aks6d1c6lem4  43026  rmxypairf1o  43739  frmy  43742  cnmetcoval  46020  dvnprodlem1  46761  dvnprodlem2  46762  volicoff  46810  voliooicof  46811  etransclem44  47093  etransclem45  47094  etransclem47  47096  hoissre  47359  hoiprodcl  47362  ovnsubaddlem1  47385  ovnhoilem2  47417  hoicoto2  47420  ovncvr2  47426  opnvonmbllem2  47448  ovolval2lem  47458  ovolval3  47462  ovolval4lem1  47464  ovolval4lem2  47465  ovolval5lem2  47468  ovnovollem1  47471  ovnovollem2  47472  smfpimbor1lem1  47613  2arymaptf  49569  rrx2xpref1o  49635  elxpcbasex2ALT  50164  swapf2f1oa  50190  swapfida  50193  fuco2eld2  50227  fucoco2  50271  pgindlem  50628