Theorem 1st2nd2 6158

Description: Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.)

Assertion

Ref	Expression
1st2nd2	|- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )

Proof of Theorem 1st2nd2

Step	Hyp	Ref	Expression
1		elxp6 6152	. 2 |- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
2	1	simplbi 272	1 |- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1349   e. wcel 2142   <.cop 3587   X. cxp 4610   ` cfv 5200   1stc1st 6121   2ndc2nd 6122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-sbc 2957  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-iota 5162  df-fun 5202  df-fv 5208  df-1st 6123  df-2nd 6124

This theorem is referenced by:  xpopth  6159  eqop  6160  2nd1st  6163  1st2nd  6164  xpmapenlem  6831  djuf1olem  7034  dfplpq2  7320  dfmpq2  7321  enqbreq2  7323  enqdc1  7328  preqlu  7438  prop  7441  elnp1st2nd  7442  cauappcvgprlemladd  7624  elreal2  7796  cnref1o  9613  frecuzrdgrrn  10368  frec2uzrdg  10369  frecuzrdgrcl  10370  frecuzrdgsuc  10374  frecuzrdgrclt  10375  frecuzrdgg  10376  frecuzrdgdomlem  10377  frecuzrdgfunlem  10379  frecuzrdgsuctlem  10383  seq3val  10418  seqvalcd  10419  eucalgval  12012  eucalginv  12014  eucalglt  12015  eucalg  12017  sqpweven  12133  2sqpwodd  12134  qnumdenbi  12150  tx1cn  13148  tx2cn  13149  txdis  13156  psmetxrge0  13211  xmetxpbl  13387