Theorem 1st2nd2 7870

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ⟨cop 4567   × cxp 5587  ‘cfv 6433  1^st c1st 7829  2^nd c2nd 7830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fv 6441  df-1st 7831  df-2nd 7832

This theorem is referenced by:  1st2ndb  7871  xpopth  7872  eqop  7873  2nd1st  7879  1st2nd  7880  opiota  7899  fimaproj  7976  disjen  8921  xpmapenlem  8931  mapunen  8933  djulf1o  9670  djurf1o  9671  djur  9677  r0weon  9768  enqbreq2  10676  nqereu  10685  lterpq  10726  elreal2  10888  cnref1o  12725  ruclem6  15944  ruclem8  15946  ruclem9  15947  ruclem12  15950  eucalgval  16287  eucalginv  16289  eucalglt  16290  eucalg  16292  qnumdenbi  16448  isstruct2  16850  xpsff1o  17278  comfffval2  17410  comfeq  17415  idfucl  17596  funcpropd  17616  coapm  17786  xpccatid  17905  1stfcl  17914  2ndfcl  17915  1st2ndprf  17923  xpcpropd  17926  evlfcl  17940  hofcl  17977  hofpropd  17985  yonedalem3  17998  gsum2dlem2  19572  mdetunilem9  21769  tx1cn  22760  tx2cn  22761  txdis  22783  txlly  22787  txnlly  22788  txhaus  22798  txkgen  22803  txconn  22840  utop3cls  23403  ucnima  23433  fmucndlem  23443  psmetxrge0  23466  imasdsf1olem  23526  cnheiborlem  24117  caublcls  24473  bcthlem1  24488  bcthlem2  24489  bcthlem4  24491  bcthlem5  24492  ovolfcl  24630  ovolfioo  24631  ovolficc  24632  ovolficcss  24633  ovolfsval  24634  ovolicc2lem1  24681  ovolicc2lem5  24685  ovolfs2  24735  uniiccdif  24742  uniioovol  24743  uniiccvol  24744  uniioombllem2a  24746  uniioombllem2  24747  uniioombllem3a  24748  uniioombllem3  24749  uniioombllem4  24750  uniioombllem5  24751  uniioombllem6  24752  dyadmbl  24764  fsumvma  26361  opreu2reuALT  30825  ofpreima  31002  ofpreima2  31003  1stmbfm  32227  2ndmbfm  32228  sibfof  32307  oddpwdcv  32322  txsconnlem  33202  mpst123  33502  bj-elid4  35339  bj-elid6  35341  poimirlem4  35781  poimirlem26  35803  poimirlem27  35804  mblfinlem1  35814  mblfinlem2  35815  ftc2nc  35859  heiborlem8  35976  dvhgrp  39121  dvhlveclem  39122  fvovco  42732  dvnprodlem1  43487  volioof  43528  fvvolioof  43530  fvvolicof  43532  etransclem44  43819  ovolval3  44185  ovolval4lem1  44187  ovolval5lem2  44191  ovnovollem1  44194  ovnovollem2  44195  smfpimbor1lem1  44332  rrx2xpref1o  46064