Theorem xp2nd 7724

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 5580	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3499	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3499	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7702	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2899	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 480	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 714	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1933	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ⟨cop 4575   × cxp 5555  ‘cfv 6357  2^nd c2nd 7690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fv 6365  df-2nd 7692

This theorem is referenced by:  offval22  7785  fimaproj  7831  disjen  8676  xpf1o  8681  xpmapenlem  8686  mapunen  8688  djur  9350  r0weon  9440  infxpenlem  9441  fseqdom  9454  axcc2lem  9860  iunfo  9963  iundom2g  9964  enqbreq2  10344  nqereu  10353  addpqf  10368  mulpqf  10370  adderpqlem  10378  mulerpqlem  10379  addassnq  10382  mulassnq  10383  distrnq  10385  mulidnq  10387  recmulnq  10388  ltsonq  10393  lterpq  10394  ltanq  10395  ltmnq  10396  ltexnq  10399  archnq  10404  elreal2  10556  cnref1o  12387  fsumcom2  15131  fprodcom2  15340  ruclem6  15590  ruclem8  15592  ruclem9  15593  ruclem10  15594  ruclem12  15596  eucalgval  15928  eucalginv  15930  eucalglt  15931  eucalgcvga  15932  eucalg  15933  xpsff1o  16842  comfffval2  16973  comfeq  16978  idfucl  17153  funcpropd  17172  fucpropd  17249  xpccatid  17440  1stfcl  17449  2ndfcl  17450  xpcpropd  17460  hofcl  17511  hofpropd  17519  yonedalem3  17532  lsmhash  18833  gsum2dlem2  19093  dprd2da  19166  evlslem4  20290  mdetunilem9  21231  tx1cn  22219  txdis  22242  txlly  22246  txnlly  22247  txhaus  22257  txkgen  22262  txconn  22299  txhmeo  22413  ptuncnv  22417  ptunhmeo  22418  xkohmeo  22425  utop2nei  22861  utop3cls  22862  imasdsf1olem  22985  cnheiborlem  23560  caubl  23913  caublcls  23914  bcthlem2  23930  bcthlem4  23932  bcthlem5  23933  ovolficcss  24072  ovoliunlem1  24105  ovoliunlem2  24106  ovolicc2lem1  24120  ovolicc2lem2  24121  ovolicc2lem3  24122  ovolicc2lem4  24123  ovolicc2lem5  24124  dyadmbl  24203  fsumvma  25791  opreu2reuALT  30242  disjxpin  30340  fsumiunle  30547  gsummpt2d  30689  cnre2csqima  31156  tpr2rico  31157  esum2dlem  31353  esumiun  31355  1stmbfm  31520  dya2iocnrect  31541  sibfof  31600  sitgaddlemb  31608  hgt750lemb  31929  satefvfmla0  32667  mvrsfpw  32755  msubff  32779  msubco  32780  msubvrs  32809  elxp8  34654  finixpnum  34879  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem29  34923  poimirlem31  34925  heicant  34929  mblfinlem1  34931  mblfinlem2  34932  ftc2nc  34978  heiborlem8  35098  dvhfvadd  38229  dvhvaddcl  38233  dvhvaddcomN  38234  dvhvaddass  38235  dvhvscacl  38241  dvhgrp  38245  dvhlveclem  38246  dibelval2nd  38290  dicelval2nd  38327  rmxypairf1o  39515  frmy  39518  cnmetcoval  41472  dvnprodlem1  42238  dvnprodlem2  42239  volicoff  42287  voliooicof  42288  etransclem44  42570  etransclem45  42571  etransclem47  42573  hoissre  42833  hoiprodcl  42836  ovnsubaddlem1  42859  ovnhoilem2  42891  hoicoto2  42894  ovncvr2  42900  opnvonmbllem2  42922  ovolval2lem  42932  ovolval3  42936  ovolval4lem1  42938  ovolval4lem2  42939  ovolval5lem2  42942  ovnovollem1  42945  ovnovollem2  42946  smfpimbor1lem1  43080  rrx2xpref1o  44712