Theorem xp2nd 7732

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 5551	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3413	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3413	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7710	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2836	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 481	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1933	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ⟨cop 4531   × cxp 5526  ‘cfv 6340  2^nd c2nd 7698

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-iota 6299  df-fun 6342  df-fv 6348  df-2nd 7700

This theorem is referenced by:  offval22  7794  fimaproj  7840  disjen  8709  xpf1o  8714  xpmapenlem  8719  mapunen  8721  djur  9394  r0weon  9485  infxpenlem  9486  fseqdom  9499  axcc2lem  9909  iunfo  10012  iundom2g  10013  enqbreq2  10393  nqereu  10402  addpqf  10417  mulpqf  10419  adderpqlem  10427  mulerpqlem  10428  addassnq  10431  mulassnq  10432  distrnq  10434  mulidnq  10436  recmulnq  10437  ltsonq  10442  lterpq  10443  ltanq  10444  ltmnq  10445  ltexnq  10448  archnq  10453  elreal2  10605  cnref1o  12438  fsumcom2  15190  fprodcom2  15399  ruclem6  15649  ruclem8  15651  ruclem9  15652  ruclem10  15653  ruclem12  15655  eucalgval  15991  eucalginv  15993  eucalglt  15994  eucalgcvga  15995  eucalg  15996  xpsff1o  16911  comfffval2  17042  comfeq  17047  idfucl  17223  funcpropd  17242  fucpropd  17319  xpccatid  17517  1stfcl  17526  2ndfcl  17527  xpcpropd  17537  hofcl  17588  hofpropd  17596  yonedalem3  17609  lsmhash  18911  gsum2dlem2  19172  dprd2da  19245  evlslem4  20850  mdetunilem9  21333  tx1cn  22322  txdis  22345  txlly  22349  txnlly  22350  txhaus  22360  txkgen  22365  txconn  22402  txhmeo  22516  ptuncnv  22520  ptunhmeo  22521  xkohmeo  22528  utop2nei  22964  utop3cls  22965  imasdsf1olem  23088  cnheiborlem  23668  caubl  24021  caublcls  24022  bcthlem2  24038  bcthlem4  24040  bcthlem5  24041  ovolficcss  24182  ovoliunlem1  24215  ovoliunlem2  24216  ovolicc2lem1  24230  ovolicc2lem2  24231  ovolicc2lem3  24232  ovolicc2lem4  24233  ovolicc2lem5  24234  dyadmbl  24313  fsumvma  25909  opreu2reuALT  30359  disjxpin  30462  2ndimaxp  30519  2ndresdju  30521  fsumiunle  30679  gsummpt2d  30847  cnre2csqima  31394  tpr2rico  31395  esum2dlem  31591  esumiun  31593  1stmbfm  31758  dya2iocnrect  31779  sibfof  31838  sitgaddlemb  31846  hgt750lemb  32167  satefvfmla0  32908  mvrsfpw  32996  msubff  33020  msubco  33021  msubvrs  33050  elxp8  35102  finixpnum  35356  poimirlem4  35375  poimirlem5  35376  poimirlem6  35377  poimirlem7  35378  poimirlem8  35379  poimirlem9  35380  poimirlem10  35381  poimirlem11  35382  poimirlem12  35383  poimirlem13  35384  poimirlem14  35385  poimirlem15  35386  poimirlem16  35387  poimirlem17  35388  poimirlem18  35389  poimirlem19  35390  poimirlem20  35391  poimirlem21  35392  poimirlem22  35393  poimirlem25  35396  poimirlem26  35397  poimirlem27  35398  poimirlem29  35400  poimirlem31  35402  heicant  35406  mblfinlem1  35408  mblfinlem2  35409  ftc2nc  35453  heiborlem8  35570  dvhfvadd  38701  dvhvaddcl  38705  dvhvaddcomN  38706  dvhvaddass  38707  dvhvscacl  38713  dvhgrp  38717  dvhlveclem  38718  dibelval2nd  38762  dicelval2nd  38799  rmxypairf1o  40260  frmy  40263  cnmetcoval  42236  dvnprodlem1  42989  dvnprodlem2  42990  volicoff  43038  voliooicof  43039  etransclem44  43321  etransclem45  43322  etransclem47  43324  hoissre  43584  hoiprodcl  43587  ovnsubaddlem1  43610  ovnhoilem2  43642  hoicoto2  43645  ovncvr2  43651  opnvonmbllem2  43673  ovolval2lem  43683  ovolval3  43687  ovolval4lem1  43689  ovolval4lem2  43690  ovolval5lem2  43693  ovnovollem1  43696  ovnovollem2  43697  smfpimbor1lem1  43831  2arymaptf  45480  rrx2xpref1o  45546