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

Theorem 1st2nd2 7368
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 7363 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)))
21simplbi 478 1 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1628  wcel 2135  cop 4323   × cxp 5260  cfv 6045  1st c1st 7327  2nd c2nd 7328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-sbc 3573  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-iota 6008  df-fun 6047  df-fv 6053  df-1st 7329  df-2nd 7330
This theorem is referenced by:  1st2ndb  7369  xpopth  7370  eqop  7371  2nd1st  7376  1st2nd  7377  opiota  7392  disjen  8278  xpmapenlem  8288  mapunen  8290  djulf1o  8942  djurf1o  8943  djur  8945  r0weon  9021  enqbreq2  9930  nqereu  9939  lterpq  9980  elreal2  10141  cnref1o  12016  ruclem6  15159  ruclem8  15161  ruclem9  15162  ruclem12  15165  eucalgval  15493  eucalginv  15495  eucalglt  15496  eucalg  15498  qnumdenbi  15650  isstruct2  16065  xpsff1o  16426  comfffval2  16558  comfeq  16563  idfucl  16738  funcpropd  16757  coapm  16918  xpccatid  17025  1stfcl  17034  2ndfcl  17035  1st2ndprf  17043  xpcpropd  17045  evlfcl  17059  hofcl  17096  hofpropd  17104  yonedalem3  17117  gsum2dlem2  18566  mdetunilem9  20624  tx1cn  21610  tx2cn  21611  txdis  21633  txlly  21637  txnlly  21638  txhaus  21648  txkgen  21653  txconn  21690  utop3cls  22252  ucnima  22282  fmucndlem  22292  psmetxrge0  22315  imasdsf1olem  22375  cnheiborlem  22950  caublcls  23303  bcthlem1  23317  bcthlem2  23318  bcthlem4  23320  bcthlem5  23321  ovolfcl  23431  ovolfioo  23432  ovolficc  23433  ovolficcss  23434  ovolfsval  23435  ovolicc2lem1  23481  ovolicc2lem5  23485  ovolfs2  23535  uniiccdif  23542  uniioovol  23543  uniiccvol  23544  uniioombllem2a  23546  uniioombllem2  23547  uniioombllem3a  23548  uniioombllem3  23549  uniioombllem4  23550  uniioombllem5  23551  uniioombllem6  23552  dyadmbl  23564  fsumvma  25133  ofpreima  29770  ofpreima2  29771  fimaproj  30205  1stmbfm  30627  2ndmbfm  30628  sibfof  30707  oddpwdcv  30722  txsconnlem  31525  mpst123  31740  bj-elid  33392  poimirlem4  33722  poimirlem26  33744  poimirlem27  33745  mblfinlem1  33755  mblfinlem2  33756  ftc2nc  33803  heiborlem8  33926  dvhgrp  36894  dvhlveclem  36895  fvovco  39876  dvnprodlem1  40660  volioof  40703  fvvolioof  40705  fvvolicof  40707  etransclem44  40994  ovolval3  41363  ovolval4lem1  41365  ovolval5lem2  41369  ovnovollem1  41372  ovnovollem2  41373  smfpimbor1lem1  41507
  Copyright terms: Public domain W3C validator