Theorem xp2nd 8017

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569  ∃wex 1808   ∈ wcel 2142  ⟨cop 4594   × cxp 5658  ‘cfv 6536  2^nd c2nd 7983

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  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 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-2nd 7985

This theorem is used by:  offval22  8081  mpof1o2d  8119  fimaproj  8129  disjen  9120  xpf1o  9125  xpmapenlem  9130  mapunen  9132  djur  9912  r0weon  10003  infxpenlem  10004  fseqdom  10017  axcc2lem  10426  iunfo  10529  iundom2g  10530  enqbreq2  10911  nqereu  10920  addpqf  10935  mulpqf  10937  adderpqlem  10945  mulerpqlem  10946  addassnq  10949  mulassnq  10950  distrnq  10952  mulidnq  10954  recmulnq  10955  ltsonq  10960  lterpq  10961  ltanq  10962  ltmnq  10963  ltexnq  10966  archnq  10971  elreal2  11123  cnref1o  13015  fsumcom2  15832  fprodcom2  16045  ruclem6  16297  ruclem8  16299  ruclem9  16300  ruclem10  16301  ruclem12  16303  eucalgval  16646  eucalginv  16648  eucalglt  16649  eucalgcvga  16650  eucalg  16651  xpsff1o  17627  comfffval2  17763  comfeq  17768  idfucl  17944  funcpropd  17965  fucpropd  18043  xpccatid  18250  1stfcl  18259  2ndfcl  18260  xpcpropd  18270  hofcl  18321  hofpropd  18329  yonedalem3  18342  lsmhash  19781  gsum2dlem2  20047  dprd2da  20120  evlslem4  22238  mdetunilem9  22788  tx1cn  23777  txdis  23800  txlly  23804  txnlly  23805  txhaus  23815  txkgen  23820  txconn  23857  txhmeo  23971  ptuncnv  23975  ptunhmeo  23976  xkohmeo  23983  utop2nei  24418  utop3cls  24419  imasdsf1olem  24541  cnheiborlem  25124  caubl  25478  caublcls  25479  bcthlem2  25495  bcthlem4  25497  bcthlem5  25498  ovolficcss  25639  ovoliunlem1  25672  ovoliunlem2  25673  ovolicc2lem1  25687  ovolicc2lem2  25688  ovolicc2lem3  25689  ovolicc2lem4  25690  ovolicc2lem5  25691  dyadmbl  25770  fsumvma  27388  opreu2reuALT  32834  disjxpin  32944  2ndimaxp  33002  2ndresdju  33005  fsumiunle  33184  gsummpt2d  33378  gsumwrd2dccatlem  33406  conjga  33499  elrgspnlem2  33572  elrgspnsubrunlem2  33577  erler  33594  rlocaddval  33598  rlocmulval  33599  mplvrpmga  33944  cnre2csqima  34310  tpr2rico  34311  esum2dlem  34491  esumiun  34493  1stmbfm  34659  dya2iocnrect  34680  sibfof  34739  sitgaddlemb  34747  hgt750lemb  35052  satefvfmla0  35918  mvrsfpw  36006  msubff  36030  msubco  36031  msubvrs  36060  elxp8  38045  finixpnum  38284  poimirlem4  38303  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem9  38308  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem29  38328  poimirlem31  38330  heicant  38334  mblfinlem1  38336  mblfinlem2  38337  ftc2nc  38381  heiborlem8  38497  dvhfvadd  41893  dvhvaddcl  41897  dvhvaddcomN  41898  dvhvaddass  41899  dvhvscacl  41905  dvhgrp  41909  dvhlveclem  41910  dibelval2nd  41954  dicelval2nd  41991  aks6d1c2p1  42913  aks6d1c3  42918  aks6d1c4  42919  aks6d1c6lem2  42966  aks6d1c6lem4  42968  rmxypairf1o  43666  frmy  43669  cnmetcoval  45947  dvnprodlem1  46688  dvnprodlem2  46689  volicoff  46737  voliooicof  46738  etransclem44  47020  etransclem45  47021  etransclem47  47023  hoissre  47286  hoiprodcl  47289  ovnsubaddlem1  47312  ovnhoilem2  47344  hoicoto2  47347  ovncvr2  47353  opnvonmbllem2  47375  ovolval2lem  47385  ovolval3  47389  ovolval4lem1  47391  ovolval4lem2  47392  ovolval5lem2  47395  ovnovollem1  47398  ovnovollem2  47399  smfpimbor1lem1  47540  2arymaptf  49460  rrx2xpref1o  49526  elxpcbasex2ALT  50057  swapf2f1oa  50083  swapfida  50086  fuco2eld2  50120  fucoco2  50164  pgindlem  50521