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

Theorem 1st2nd2 6746
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

Proof of Theorem 1st2nd2
StepHypRef Expression
1 elxp6 6741 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  e.wcel 1758  <.cop 3999  X.cxp 4955  `cfv 5537   c1st 6708   c2nd 6709
This theorem is referenced by:  1st2ndb  6747  xpopth  6748  eqop  6749  2nd1st  6752  1st2nd  6753  opiota  6766  disjen  7602  xpmapenlem  7612  mapunen  7614  r0weon  8316  enqbreq2  9226  nqereu  9235  lterpq  9276  elreal2  9436  cnref1o  11125  ruclem6  13675  ruclem8  13677  ruclem9  13678  ruclem12  13681  eucalgval  13915  eucalginv  13917  eucalglt  13918  eucalg  13920  qnumdenbi  13980  isstruct2  14341  xpsff1o  14665  comfffval2  14799  comfeq  14804  idfucl  14950  funcpropd  14969  coapm  15098  xpccatid  15157  1stfcl  15166  2ndfcl  15167  1st2ndprf  15175  xpcpropd  15177  evlfcl  15191  hofcl  15228  hofpropd  15236  yonedalem3  15249  gsum2dlem2  16631  gsum2dOLD  16633  mdetunilem9  18694  tx1cn  19581  tx2cn  19582  txdis  19604  txlly  19608  txnlly  19609  txhaus  19619  txkgen  19624  txcon  19661  utop3cls  20225  ucnima  20255  fmucndlem  20265  psmetxrge0  20288  imasdsf1olem  20347  cnheiborlem  20925  caublcls  21218  bcthlem1  21234  bcthlem2  21235  bcthlem4  21237  bcthlem5  21238  ovolfcl  21349  ovolfioo  21350  ovolficc  21351  ovolficcss  21352  ovolfsval  21353  ovolicc2lem1  21399  ovolicc2lem5  21403  ovolfs2  21451  uniiccdif  21458  uniioovol  21459  uniiccvol  21460  uniioombllem2a  21462  uniioombllem2  21463  uniioombllem3a  21464  uniioombllem3  21465  uniioombllem4  21466  uniioombllem5  21467  uniioombllem6  21468  dyadmbl  21480  fsumvma  22952  ofpreima  26451  ofpreima2  26452  1stmbfm  27131  2ndmbfm  27132  sibfof  27182  oddpwdcv  27194  txsconlem  27585  mblfinlem1  28888  mblfinlem2  28889  ftc2nc  28936  heiborlem8  29177  wlkcpr  31167  bj-elid  33371  dvhgrp  35603  dvhlveclem  35604
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 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505
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 2650  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-mpt 4469  df-id 4753  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-iota 5500  df-fun 5539  df-fv 5545  df-1st 6710  df-2nd 6711
  Copyright terms: Public domain W3C validator