Theorem 1st2nd2 7843

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   × cxp 5578  ‘cfv 6418  1^st c1st 7802  2^nd c2nd 7803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fv 6426  df-1st 7804  df-2nd 7805

This theorem is referenced by:  1st2ndb  7844  xpopth  7845  eqop  7846  2nd1st  7852  1st2nd  7853  opiota  7872  fimaproj  7947  disjen  8870  xpmapenlem  8880  mapunen  8882  djulf1o  9601  djurf1o  9602  djur  9608  r0weon  9699  enqbreq2  10607  nqereu  10616  lterpq  10657  elreal2  10819  cnref1o  12654  ruclem6  15872  ruclem8  15874  ruclem9  15875  ruclem12  15878  eucalgval  16215  eucalginv  16217  eucalglt  16218  eucalg  16220  qnumdenbi  16376  isstruct2  16778  xpsff1o  17195  comfffval2  17327  comfeq  17332  idfucl  17512  funcpropd  17532  coapm  17702  xpccatid  17821  1stfcl  17830  2ndfcl  17831  1st2ndprf  17839  xpcpropd  17842  evlfcl  17856  hofcl  17893  hofpropd  17901  yonedalem3  17914  gsum2dlem2  19487  mdetunilem9  21677  tx1cn  22668  tx2cn  22669  txdis  22691  txlly  22695  txnlly  22696  txhaus  22706  txkgen  22711  txconn  22748  utop3cls  23311  ucnima  23341  fmucndlem  23351  psmetxrge0  23374  imasdsf1olem  23434  cnheiborlem  24023  caublcls  24378  bcthlem1  24393  bcthlem2  24394  bcthlem4  24396  bcthlem5  24397  ovolfcl  24535  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovolfsval  24539  ovolicc2lem1  24586  ovolicc2lem5  24590  ovolfs2  24640  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem2a  24651  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombllem6  24657  dyadmbl  24669  fsumvma  26266  opreu2reuALT  30726  ofpreima  30904  ofpreima2  30905  1stmbfm  32127  2ndmbfm  32128  sibfof  32207  oddpwdcv  32222  txsconnlem  33102  mpst123  33402  bj-elid4  35266  bj-elid6  35268  poimirlem4  35708  poimirlem26  35730  poimirlem27  35731  mblfinlem1  35741  mblfinlem2  35742  ftc2nc  35786  heiborlem8  35903  dvhgrp  39048  dvhlveclem  39049  fvovco  42621  dvnprodlem1  43377  volioof  43418  fvvolioof  43420  fvvolicof  43422  etransclem44  43709  ovolval3  44075  ovolval4lem1  44077  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  smfpimbor1lem1  44219  rrx2xpref1o  45952