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

Theorem 1st2nd2 6818
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 6813 . 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 1379    e. wcel 1767   <.cop 4033    X. cxp 4997   ` cfv 5586   1stc1st 6779   2ndc2nd 6780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5549  df-fun 5588  df-fv 5594  df-1st 6781  df-2nd 6782
This theorem is referenced by:  1st2ndb  6819  xpopth  6820  eqop  6821  2nd1st  6826  1st2nd  6827  opiota  6840  disjen  7671  xpmapenlem  7681  mapunen  7683  r0weon  8386  enqbreq2  9294  nqereu  9303  lterpq  9344  elreal2  9505  cnref1o  11211  ruclem6  13825  ruclem8  13827  ruclem9  13828  ruclem12  13831  eucalgval  14066  eucalginv  14068  eucalglt  14069  eucalg  14071  qnumdenbi  14132  isstruct2  14495  xpsff1o  14819  comfffval2  14953  comfeq  14958  idfucl  15104  funcpropd  15123  coapm  15252  xpccatid  15311  1stfcl  15320  2ndfcl  15321  1st2ndprf  15329  xpcpropd  15331  evlfcl  15345  hofcl  15382  hofpropd  15390  yonedalem3  15403  gsum2dlem2  16789  gsum2dOLD  16791  mdetunilem9  18889  tx1cn  19845  tx2cn  19846  txdis  19868  txlly  19872  txnlly  19873  txhaus  19883  txkgen  19888  txcon  19925  utop3cls  20489  ucnima  20519  fmucndlem  20529  psmetxrge0  20552  imasdsf1olem  20611  cnheiborlem  21189  caublcls  21482  bcthlem1  21498  bcthlem2  21499  bcthlem4  21501  bcthlem5  21502  ovolfcl  21613  ovolfioo  21614  ovolficc  21615  ovolficcss  21616  ovolfsval  21617  ovolicc2lem1  21663  ovolicc2lem5  21667  ovolfs2  21715  uniiccdif  21722  uniioovol  21723  uniiccvol  21724  uniioombllem2a  21726  uniioombllem2  21727  uniioombllem3a  21728  uniioombllem3  21729  uniioombllem4  21730  uniioombllem5  21731  uniioombllem6  21732  dyadmbl  21744  fsumvma  23216  wlkcpr  24205  isrusgusrgcl  24609  isrgrac  24610  0eusgraiff0rgracl  24617  ofpreima  27179  ofpreima2  27180  fimaproj  27499  1stmbfm  27871  2ndmbfm  27872  sibfof  27922  oddpwdcv  27934  txsconlem  28325  mblfinlem1  29628  mblfinlem2  29629  ftc2nc  29676  heiborlem8  29917  uhgrasiz  31863  isfusgracl  31895  isfusgraclALT  31897  bj-elid  33672  dvhgrp  35904  dvhlveclem  35905
  Copyright terms: Public domain W3C validator