Theorem 1st2nd2 7977

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ⟨cop 4568   × cxp 5623  ‘cfv 6492  1^st c1st 7936  2^nd c2nd 7937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7938  df-2nd 7939

This theorem is referenced by:  1st2ndb  7978  xpopth  7979  eqop  7980  2nd1st  7987  1st2nd  7988  opiota  8008  fimaproj  8082  disjen  9069  xpmapenlem  9079  mapunen  9081  djulf1o  9834  djurf1o  9835  djur  9841  r0weon  9932  enqbreq2  10841  nqereu  10850  lterpq  10891  elreal2  11053  cnref1o  12933  ruclem6  16200  ruclem8  16202  ruclem9  16203  ruclem12  16206  eucalgval  16549  eucalginv  16551  eucalglt  16552  eucalg  16554  qnumdenbi  16712  isstruct2  17117  xpsff1o  17529  comfffval2  17665  comfeq  17670  idfucl  17846  funcpropd  17867  coapm  18036  xpccatid  18152  1stfcl  18161  2ndfcl  18162  1st2ndprf  18170  xpcpropd  18172  evlfcl  18186  hofcl  18223  hofpropd  18231  yonedalem3  18244  gsum2dlem2  19944  mdetunilem9  22610  tx1cn  23599  tx2cn  23600  txdis  23622  txlly  23626  txnlly  23627  txhaus  23637  txkgen  23642  txconn  23679  utop3cls  24241  ucnima  24270  fmucndlem  24280  psmetxrge0  24303  imasdsf1olem  24363  cnheiborlem  24946  caublcls  25301  bcthlem1  25316  bcthlem2  25317  bcthlem4  25319  bcthlem5  25320  ovolfcl  25458  ovolfioo  25459  ovolficc  25460  ovolficcss  25461  ovolfsval  25462  ovolicc2lem1  25509  ovolicc2lem5  25513  ovolfs2  25563  uniiccdif  25570  uniioovol  25571  uniiccvol  25572  uniioombllem2a  25574  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  uniioombllem6  25580  dyadmbl  25592  fsumvma  27201  opreu2reuALT  32571  ofpreima  32764  ofpreima2  32765  elrgspnsubrunlem2  33336  erler  33353  1stmbfm  34451  2ndmbfm  34452  sibfof  34531  oddpwdcv  34546  txsconnlem  35475  mpst123  35775  bj-elid4  37535  bj-elid6  37537  poimirlem4  37998  poimirlem26  38020  poimirlem27  38021  mblfinlem1  38031  mblfinlem2  38032  ftc2nc  38076  heiborlem8  38192  dvhgrp  41606  dvhlveclem  41607  fvovco  45647  dvnprodlem1  46396  volioof  46437  fvvolioof  46439  fvvolicof  46441  etransclem44  46728  ovolval3  47097  ovolval4lem1  47099  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107  smfpimbor1lem1  47248  rrx2xpref1o  49216  2oppf  49629  eloppf  49630  funcoppc5  49642  swapf2f1oa  49774  swapfida  49777  swapffunca  49781  swapfiso  49782  cofuswapf1  49791  cofuswapf2  49792  fuco2eld2  49811  fuco11b  49834  fuco11bALT  49835  fucoco2  49855  fucofunca  49857  fucolid  49858  fucorid  49859  precofvalALT  49865  reldmlan2  50114  reldmran2  50115  rellan  50120  relran  50121  ranval3  50128  ranrcl4lem  50135  ranup  50139