Theorem 1st2nd2 5945

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 5940	. 2 |- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
2	1	simplbi 268	1 |- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289   e. wcel 1438   <.cop 3449   X. cxp 4436   ` cfv 5015   1stc1st 5909   2ndc2nd 5910

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036  ax-un 4260

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2841  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-br 3846  df-opab 3900  df-mpt 3901  df-id 4120  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-iota 4980  df-fun 5017  df-fv 5023  df-1st 5911  df-2nd 5912

This theorem is referenced by:  xpopth  5946  eqop  5947  2nd1st  5950  1st2nd  5951  xpmapenlem  6563  djuf1olem  6743  djur  6755  dfplpq2  6911  dfmpq2  6912  enqbreq2  6914  enqdc1  6919  preqlu  7029  prop  7032  elnp1st2nd  7033  cauappcvgprlemladd  7215  elreal2  7366  cnref1o  9131  frecuzrdgrrn  9811  frec2uzrdg  9812  frecuzrdgrcl  9813  frecuzrdgsuc  9817  frecuzrdgrclt  9818  frecuzrdgg  9819  frecuzrdgdomlem  9820  frecuzrdgfunlem  9822  frecuzrdgsuctlem  9826  iseqvalt  9869  seq3val  9870  eucalgval  11310  eucalginv  11312  eucalglt  11313  eucialg  11315  sqpweven  11427  2sqpwodd  11428  qnumdenbi  11444