Theorem xp2nd 8045

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105  ⟨cop 4636   × cxp 5686  ‘cfv 6562  2^nd c2nd 8011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fv 6570  df-2nd 8013

This theorem is referenced by:  offval22  8111  fimaproj  8158  disjen  9172  xpf1o  9177  xpmapenlem  9182  mapunen  9184  djur  9956  r0weon  10049  infxpenlem  10050  fseqdom  10063  axcc2lem  10473  iunfo  10576  iundom2g  10577  enqbreq2  10957  nqereu  10966  addpqf  10981  mulpqf  10983  adderpqlem  10991  mulerpqlem  10992  addassnq  10995  mulassnq  10996  distrnq  10998  mulidnq  11000  recmulnq  11001  ltsonq  11006  lterpq  11007  ltanq  11008  ltmnq  11009  ltexnq  11012  archnq  11017  elreal2  11169  cnref1o  13024  fsumcom2  15806  fprodcom2  16016  ruclem6  16267  ruclem8  16269  ruclem9  16270  ruclem10  16271  ruclem12  16273  eucalgval  16615  eucalginv  16617  eucalglt  16618  eucalgcvga  16619  eucalg  16620  xpsff1o  17613  comfffval2  17745  comfeq  17750  idfucl  17931  funcpropd  17953  fucpropd  18033  xpccatid  18243  1stfcl  18252  2ndfcl  18253  xpcpropd  18264  hofcl  18315  hofpropd  18323  yonedalem3  18336  lsmhash  19737  gsum2dlem2  20003  dprd2da  20076  evlslem4  22117  mdetunilem9  22641  tx1cn  23632  txdis  23655  txlly  23659  txnlly  23660  txhaus  23670  txkgen  23675  txconn  23712  txhmeo  23826  ptuncnv  23830  ptunhmeo  23831  xkohmeo  23838  utop2nei  24274  utop3cls  24275  imasdsf1olem  24398  cnheiborlem  24999  caubl  25355  caublcls  25356  bcthlem2  25372  bcthlem4  25374  bcthlem5  25375  ovolficcss  25517  ovoliunlem1  25550  ovoliunlem2  25551  ovolicc2lem1  25565  ovolicc2lem2  25566  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2lem5  25569  dyadmbl  25648  fsumvma  27271  opreu2reuALT  32504  disjxpin  32607  2ndimaxp  32662  2ndresdju  32665  fsumiunle  32835  gsummpt2d  33034  gsumwrd2dccatlem  33051  elrgspnlem2  33232  erler  33251  rlocaddval  33254  rlocmulval  33255  cnre2csqima  33871  tpr2rico  33872  esum2dlem  34072  esumiun  34074  1stmbfm  34241  dya2iocnrect  34262  sibfof  34321  sitgaddlemb  34329  hgt750lemb  34649  satefvfmla0  35402  mvrsfpw  35490  msubff  35514  msubco  35515  msubvrs  35544  elxp8  37353  finixpnum  37591  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem31  37637  heicant  37641  mblfinlem1  37643  mblfinlem2  37644  ftc2nc  37688  heiborlem8  37804  dvhfvadd  41073  dvhvaddcl  41077  dvhvaddcomN  41078  dvhvaddass  41079  dvhvscacl  41085  dvhgrp  41089  dvhlveclem  41090  dibelval2nd  41134  dicelval2nd  41171  aks6d1c2p1  42099  aks6d1c3  42104  aks6d1c4  42105  aks6d1c6lem2  42152  aks6d1c6lem4  42154  f1o2d2  42252  rmxypairf1o  42899  frmy  42902  cnmetcoval  45144  dvnprodlem1  45901  dvnprodlem2  45902  volicoff  45950  voliooicof  45951  etransclem44  46233  etransclem45  46234  etransclem47  46236  hoissre  46499  hoiprodcl  46502  ovnsubaddlem1  46525  ovnhoilem2  46557  hoicoto2  46560  ovncvr2  46566  opnvonmbllem2  46588  ovolval2lem  46598  ovolval3  46602  ovolval4lem1  46604  ovolval4lem2  46605  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  smfpimbor1lem1  46753  2arymaptf  48501  rrx2xpref1o  48567  pgindlem  48945