Theorem 1st2nd2 8052

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ⟨cop 4637   × cxp 5687  ‘cfv 6563  1^st c1st 8011  2^nd c2nd 8012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fv 6571  df-1st 8013  df-2nd 8014

This theorem is referenced by:  1st2ndb  8053  xpopth  8054  eqop  8055  2nd1st  8062  1st2nd  8063  opiota  8083  fimaproj  8159  disjen  9173  xpmapenlem  9183  mapunen  9185  djulf1o  9950  djurf1o  9951  djur  9957  r0weon  10050  enqbreq2  10958  nqereu  10967  lterpq  11008  elreal2  11170  cnref1o  13025  ruclem6  16268  ruclem8  16270  ruclem9  16271  ruclem12  16274  eucalgval  16616  eucalginv  16618  eucalglt  16619  eucalg  16621  qnumdenbi  16778  isstruct2  17183  xpsff1o  17614  comfffval2  17746  comfeq  17751  idfucl  17932  funcpropd  17954  coapm  18125  xpccatid  18244  1stfcl  18253  2ndfcl  18254  1st2ndprf  18262  xpcpropd  18265  evlfcl  18279  hofcl  18316  hofpropd  18324  yonedalem3  18337  gsum2dlem2  20004  mdetunilem9  22642  tx1cn  23633  tx2cn  23634  txdis  23656  txlly  23660  txnlly  23661  txhaus  23671  txkgen  23676  txconn  23713  utop3cls  24276  ucnima  24306  fmucndlem  24316  psmetxrge0  24339  imasdsf1olem  24399  cnheiborlem  25000  caublcls  25357  bcthlem1  25372  bcthlem2  25373  bcthlem4  25375  bcthlem5  25376  ovolfcl  25515  ovolfioo  25516  ovolficc  25517  ovolficcss  25518  ovolfsval  25519  ovolicc2lem1  25566  ovolicc2lem5  25570  ovolfs2  25620  uniiccdif  25627  uniioovol  25628  uniiccvol  25629  uniioombllem2a  25631  uniioombllem2  25632  uniioombllem3a  25633  uniioombllem3  25634  uniioombllem4  25635  uniioombllem5  25636  uniioombllem6  25637  dyadmbl  25649  fsumvma  27272  opreu2reuALT  32505  ofpreima  32682  ofpreima2  32683  erler  33252  1stmbfm  34242  2ndmbfm  34243  sibfof  34322  oddpwdcv  34337  txsconnlem  35225  mpst123  35525  bj-elid4  37151  bj-elid6  37153  poimirlem4  37611  poimirlem26  37633  poimirlem27  37634  mblfinlem1  37644  mblfinlem2  37645  ftc2nc  37689  heiborlem8  37805  dvhgrp  41090  dvhlveclem  41091  fvovco  45136  dvnprodlem1  45902  volioof  45943  fvvolioof  45945  fvvolicof  45947  etransclem44  46234  ovolval3  46603  ovolval4lem1  46605  ovolval5lem2  46609  ovnovollem1  46612  ovnovollem2  46613  smfpimbor1lem1  46754  rrx2xpref1o  48568