Theorem 1st2nd2 7966

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 7961	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))
2	1	simplbi 497	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4581   × cxp 5617  ‘cfv 6486  1^st c1st 7925  2^nd c2nd 7926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fv 6494  df-1st 7927  df-2nd 7928

This theorem is referenced by:  1st2ndb  7967  xpopth  7968  eqop  7969  2nd1st  7976  1st2nd  7977  opiota  7997  fimaproj  8071  disjen  9054  xpmapenlem  9064  mapunen  9066  djulf1o  9812  djurf1o  9813  djur  9819  r0weon  9910  enqbreq2  10818  nqereu  10827  lterpq  10868  elreal2  11030  cnref1o  12885  ruclem6  16146  ruclem8  16148  ruclem9  16149  ruclem12  16152  eucalgval  16495  eucalginv  16497  eucalglt  16498  eucalg  16500  qnumdenbi  16657  isstruct2  17062  xpsff1o  17473  comfffval2  17609  comfeq  17614  idfucl  17790  funcpropd  17811  coapm  17980  xpccatid  18096  1stfcl  18105  2ndfcl  18106  1st2ndprf  18114  xpcpropd  18116  evlfcl  18130  hofcl  18167  hofpropd  18175  yonedalem3  18188  gsum2dlem2  19885  mdetunilem9  22536  tx1cn  23525  tx2cn  23526  txdis  23548  txlly  23552  txnlly  23553  txhaus  23563  txkgen  23568  txconn  23605  utop3cls  24167  ucnima  24196  fmucndlem  24206  psmetxrge0  24229  imasdsf1olem  24289  cnheiborlem  24881  caublcls  25237  bcthlem1  25252  bcthlem2  25253  bcthlem4  25255  bcthlem5  25256  ovolfcl  25395  ovolfioo  25396  ovolficc  25397  ovolficcss  25398  ovolfsval  25399  ovolicc2lem1  25446  ovolicc2lem5  25450  ovolfs2  25500  uniiccdif  25507  uniioovol  25508  uniiccvol  25509  uniioombllem2a  25511  uniioombllem2  25512  uniioombllem3a  25513  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  uniioombllem6  25517  dyadmbl  25529  fsumvma  27152  opreu2reuALT  32458  ofpreima  32649  ofpreima2  32650  elrgspnsubrunlem2  33222  erler  33239  1stmbfm  34294  2ndmbfm  34295  sibfof  34374  oddpwdcv  34389  txsconnlem  35305  mpst123  35605  bj-elid4  37233  bj-elid6  37235  poimirlem4  37685  poimirlem26  37707  poimirlem27  37708  mblfinlem1  37718  mblfinlem2  37719  ftc2nc  37763  heiborlem8  37879  dvhgrp  41227  dvhlveclem  41228  fvovco  45315  dvnprodlem1  46069  volioof  46110  fvvolioof  46112  fvvolicof  46114  etransclem44  46401  ovolval3  46770  ovolval4lem1  46772  ovolval5lem2  46776  ovnovollem1  46779  ovnovollem2  46780  smfpimbor1lem1  46921  rrx2xpref1o  48844  2oppf  49258  eloppf  49259  funcoppc5  49271  swapf2f1oa  49403  swapfida  49406  swapffunca  49410  swapfiso  49411  cofuswapf1  49420  cofuswapf2  49421  fuco2eld2  49440  fuco11b  49463  fuco11bALT  49464  fucoco2  49484  fucofunca  49486  fucolid  49487  fucorid  49488  precofvalALT  49494  reldmlan2  49743  reldmran2  49744  rellan  49749  relran  49750  ranval3  49757  ranrcl4lem  49764  ranup  49768