Theorem 1st2nd2 7972

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   × cxp 5620  ‘cfv 6490  1^st c1st 7931  2^nd c2nd 7932

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 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-1st 7933  df-2nd 7934

This theorem is referenced by:  1st2ndb  7973  xpopth  7974  eqop  7975  2nd1st  7982  1st2nd  7983  opiota  8003  fimaproj  8076  disjen  9063  xpmapenlem  9073  mapunen  9075  djulf1o  9825  djurf1o  9826  djur  9832  r0weon  9923  enqbreq2  10832  nqereu  10841  lterpq  10882  elreal2  11044  cnref1o  12899  ruclem6  16161  ruclem8  16163  ruclem9  16164  ruclem12  16167  eucalgval  16510  eucalginv  16512  eucalglt  16513  eucalg  16515  qnumdenbi  16672  isstruct2  17077  xpsff1o  17489  comfffval2  17625  comfeq  17630  idfucl  17806  funcpropd  17827  coapm  17996  xpccatid  18112  1stfcl  18121  2ndfcl  18122  1st2ndprf  18130  xpcpropd  18132  evlfcl  18146  hofcl  18183  hofpropd  18191  yonedalem3  18204  gsum2dlem2  19904  mdetunilem9  22563  tx1cn  23552  tx2cn  23553  txdis  23575  txlly  23579  txnlly  23580  txhaus  23590  txkgen  23595  txconn  23632  utop3cls  24194  ucnima  24223  fmucndlem  24233  psmetxrge0  24256  imasdsf1olem  24316  cnheiborlem  24899  caublcls  25254  bcthlem1  25269  bcthlem2  25270  bcthlem4  25272  bcthlem5  25273  ovolfcl  25411  ovolfioo  25412  ovolficc  25413  ovolficcss  25414  ovolfsval  25415  ovolicc2lem1  25462  ovolicc2lem5  25466  ovolfs2  25516  uniiccdif  25523  uniioovol  25524  uniiccvol  25525  uniioombllem2a  25527  uniioombllem2  25528  uniioombllem3a  25529  uniioombllem3  25530  uniioombllem4  25531  uniioombllem5  25532  uniioombllem6  25533  dyadmbl  25545  fsumvma  27164  opreu2reuALT  32535  ofpreima  32727  ofpreima2  32728  elrgspnsubrunlem2  33314  erler  33331  1stmbfm  34410  2ndmbfm  34411  sibfof  34490  oddpwdcv  34505  txsconnlem  35428  mpst123  35728  bj-elid4  37480  bj-elid6  37482  poimirlem4  37936  poimirlem26  37958  poimirlem27  37959  mblfinlem1  37969  mblfinlem2  37970  ftc2nc  38014  heiborlem8  38130  dvhgrp  41544  dvhlveclem  41545  fvovco  45626  dvnprodlem1  46378  volioof  46419  fvvolioof  46421  fvvolicof  46423  etransclem44  46710  ovolval3  47079  ovolval4lem1  47081  ovolval5lem2  47085  ovnovollem1  47088  ovnovollem2  47089  smfpimbor1lem1  47230  rrx2xpref1o  49152  2oppf  49565  eloppf  49566  funcoppc5  49578  swapf2f1oa  49710  swapfida  49713  swapffunca  49717  swapfiso  49718  cofuswapf1  49727  cofuswapf2  49728  fuco2eld2  49747  fuco11b  49770  fuco11bALT  49771  fucoco2  49791  fucofunca  49793  fucolid  49794  fucorid  49795  precofvalALT  49801  reldmlan2  50050  reldmran2  50051  rellan  50056  relran  50057  ranval3  50064  ranrcl4lem  50071  ranup  50075