Theorem 1st2nd2 7982

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

Step	Hyp	Ref	Expression
1		elxp6 7977	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))
2	1	simplbi 496	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4588   × cxp 5630  ‘cfv 6500  1^st c1st 7941  2^nd c2nd 7942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-1st 7943  df-2nd 7944

This theorem is referenced by:  1st2ndb  7983  xpopth  7984  eqop  7985  2nd1st  7992  1st2nd  7993  opiota  8013  fimaproj  8087  disjen  9074  xpmapenlem  9084  mapunen  9086  djulf1o  9836  djurf1o  9837  djur  9843  r0weon  9934  enqbreq2  10843  nqereu  10852  lterpq  10893  elreal2  11055  cnref1o  12910  ruclem6  16172  ruclem8  16174  ruclem9  16175  ruclem12  16178  eucalgval  16521  eucalginv  16523  eucalglt  16524  eucalg  16526  qnumdenbi  16683  isstruct2  17088  xpsff1o  17500  comfffval2  17636  comfeq  17641  idfucl  17817  funcpropd  17838  coapm  18007  xpccatid  18123  1stfcl  18132  2ndfcl  18133  1st2ndprf  18141  xpcpropd  18143  evlfcl  18157  hofcl  18194  hofpropd  18202  yonedalem3  18215  gsum2dlem2  19912  mdetunilem9  22576  tx1cn  23565  tx2cn  23566  txdis  23588  txlly  23592  txnlly  23593  txhaus  23603  txkgen  23608  txconn  23645  utop3cls  24207  ucnima  24236  fmucndlem  24246  psmetxrge0  24269  imasdsf1olem  24329  cnheiborlem  24921  caublcls  25277  bcthlem1  25292  bcthlem2  25293  bcthlem4  25295  bcthlem5  25296  ovolfcl  25435  ovolfioo  25436  ovolficc  25437  ovolficcss  25438  ovolfsval  25439  ovolicc2lem1  25486  ovolicc2lem5  25490  ovolfs2  25540  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2a  25551  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombllem6  25557  dyadmbl  25569  fsumvma  27192  opreu2reuALT  32562  ofpreima  32754  ofpreima2  32755  elrgspnsubrunlem2  33341  erler  33358  1stmbfm  34437  2ndmbfm  34438  sibfof  34517  oddpwdcv  34532  txsconnlem  35453  mpst123  35753  bj-elid4  37417  bj-elid6  37419  poimirlem4  37869  poimirlem26  37891  poimirlem27  37892  mblfinlem1  37902  mblfinlem2  37903  ftc2nc  37947  heiborlem8  38063  dvhgrp  41477  dvhlveclem  41478  fvovco  45546  dvnprodlem1  46298  volioof  46339  fvvolioof  46341  fvvolicof  46343  etransclem44  46630  ovolval3  46999  ovolval4lem1  47001  ovolval5lem2  47005  ovnovollem1  47008  ovnovollem2  47009  smfpimbor1lem1  47150  rrx2xpref1o  49072  2oppf  49485  eloppf  49486  funcoppc5  49498  swapf2f1oa  49630  swapfida  49633  swapffunca  49637  swapfiso  49638  cofuswapf1  49647  cofuswapf2  49648  fuco2eld2  49667  fuco11b  49690  fuco11bALT  49691  fucoco2  49711  fucofunca  49713  fucolid  49714  fucorid  49715  precofvalALT  49721  reldmlan2  49970  reldmran2  49971  rellan  49976  relran  49977  ranval3  49984  ranrcl4lem  49991  ranup  49995