MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1st2nd2 Structured version   Unicode version

Theorem 1st2nd2 6722
Description: Reconstruction of a member of a Cartesian 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
StepHypRef Expression
1 elxp6 6717 . 2  |-  ( A  e.  ( B  X.  C )  <->  ( A  =  <. ( 1st `  A
) ,  ( 2nd `  A ) >.  /\  (
( 1st `  A
)  e.  B  /\  ( 2nd `  A )  e.  C ) ) )
21simplbi 460 1  |-  ( A  e.  ( B  X.  C )  ->  A  =  <. ( 1st `  A
) ,  ( 2nd `  A ) >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   <.cop 3990    X. cxp 4945   ` cfv 5525   1stc1st 6684   2ndc2nd 6685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-iota 5488  df-fun 5527  df-fv 5533  df-1st 6686  df-2nd 6687
This theorem is referenced by:  1st2ndb  6723  xpopth  6724  eqop  6725  2nd1st  6728  1st2nd  6729  opiota  6742  disjen  7577  xpmapenlem  7587  mapunen  7589  r0weon  8289  enqbreq2  9199  nqereu  9208  lterpq  9249  elreal2  9409  cnref1o  11096  ruclem6  13634  ruclem8  13636  ruclem9  13637  ruclem12  13640  eucalgval  13874  eucalginv  13876  eucalglt  13877  eucalg  13879  qnumdenbi  13939  isstruct2  14300  xpsff1o  14624  comfffval2  14758  comfeq  14763  idfucl  14909  funcpropd  14928  coapm  15057  xpccatid  15116  1stfcl  15125  2ndfcl  15126  1st2ndprf  15134  xpcpropd  15136  evlfcl  15150  hofcl  15187  hofpropd  15195  yonedalem3  15208  gsum2dlem2  16583  gsum2dOLD  16585  mdetunilem9  18557  tx1cn  19313  tx2cn  19314  txdis  19336  txlly  19340  txnlly  19341  txhaus  19351  txkgen  19356  txcon  19393  utop3cls  19957  ucnima  19987  fmucndlem  19997  psmetxrge0  20020  imasdsf1olem  20079  cnheiborlem  20657  caublcls  20950  bcthlem1  20966  bcthlem2  20967  bcthlem4  20969  bcthlem5  20970  ovolfcl  21081  ovolfioo  21082  ovolficc  21083  ovolficcss  21084  ovolfsval  21085  ovolicc2lem1  21131  ovolicc2lem5  21135  ovolfs2  21183  uniiccdif  21190  uniioovol  21191  uniiccvol  21192  uniioombllem2a  21194  uniioombllem2  21195  uniioombllem3a  21196  uniioombllem3  21197  uniioombllem4  21198  uniioombllem5  21199  uniioombllem6  21200  dyadmbl  21212  fsumvma  22684  ofpreima  26134  ofpreima2  26135  1stmbfm  26818  2ndmbfm  26819  sibfof  26869  oddpwdcv  26881  txsconlem  27272  mblfinlem1  28575  mblfinlem2  28576  ftc2nc  28623  heiborlem8  28864  wlkcpr  30437  bj-elid  32843  dvhgrp  35075  dvhlveclem  35076
  Copyright terms: Public domain W3C validator