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

Theorem 1st2nd2 7961
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 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)

Proof of Theorem 1st2nd2
StepHypRef Expression
1 elxp6 7956 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)))
21simplbi 499 1 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  cop 4593   × cxp 5632  cfv 6497  1st c1st 7920  2nd c2nd 7921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-1st 7922  df-2nd 7923
This theorem is referenced by:  1st2ndb  7962  xpopth  7963  eqop  7964  2nd1st  7971  1st2nd  7972  opiota  7992  fimaproj  8068  disjen  9079  xpmapenlem  9089  mapunen  9091  djulf1o  9849  djurf1o  9850  djur  9856  r0weon  9949  enqbreq2  10857  nqereu  10866  lterpq  10907  elreal2  11069  cnref1o  12911  ruclem6  16118  ruclem8  16120  ruclem9  16121  ruclem12  16124  eucalgval  16459  eucalginv  16461  eucalglt  16462  eucalg  16464  qnumdenbi  16620  isstruct2  17022  xpsff1o  17450  comfffval2  17582  comfeq  17587  idfucl  17768  funcpropd  17788  coapm  17958  xpccatid  18077  1stfcl  18086  2ndfcl  18087  1st2ndprf  18095  xpcpropd  18098  evlfcl  18112  hofcl  18149  hofpropd  18157  yonedalem3  18170  gsum2dlem2  19749  mdetunilem9  21972  tx1cn  22963  tx2cn  22964  txdis  22986  txlly  22990  txnlly  22991  txhaus  23001  txkgen  23006  txconn  23043  utop3cls  23606  ucnima  23636  fmucndlem  23646  psmetxrge0  23669  imasdsf1olem  23729  cnheiborlem  24320  caublcls  24676  bcthlem1  24691  bcthlem2  24692  bcthlem4  24694  bcthlem5  24695  ovolfcl  24833  ovolfioo  24834  ovolficc  24835  ovolficcss  24836  ovolfsval  24837  ovolicc2lem1  24884  ovolicc2lem5  24888  ovolfs2  24938  uniiccdif  24945  uniioovol  24946  uniiccvol  24947  uniioombllem2a  24949  uniioombllem2  24950  uniioombllem3a  24951  uniioombllem3  24952  uniioombllem4  24953  uniioombllem5  24954  uniioombllem6  24955  dyadmbl  24967  fsumvma  26564  opreu2reuALT  31408  ofpreima  31584  ofpreima2  31585  1stmbfm  32863  2ndmbfm  32864  sibfof  32943  oddpwdcv  32958  txsconnlem  33837  mpst123  34137  bj-elid4  35642  bj-elid6  35644  poimirlem4  36085  poimirlem26  36107  poimirlem27  36108  mblfinlem1  36118  mblfinlem2  36119  ftc2nc  36163  heiborlem8  36280  dvhgrp  39573  dvhlveclem  39574  fvovco  43420  dvnprodlem1  44194  volioof  44235  fvvolioof  44237  fvvolicof  44239  etransclem44  44526  ovolval3  44895  ovolval4lem1  44897  ovolval5lem2  44901  ovnovollem1  44904  ovnovollem2  44905  smfpimbor1lem1  45046  rrx2xpref1o  46811
  Copyright terms: Public domain W3C validator