Theorem 1st2nd2 7974

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 7969	. 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 5622  ‘cfv 6492  1^st c1st 7933  2^nd c2nd 7934

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 5370  ax-un 7682

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 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7935  df-2nd 7936

This theorem is referenced by:  1st2ndb  7975  xpopth  7976  eqop  7977  2nd1st  7984  1st2nd  7985  opiota  8005  fimaproj  8078  disjen  9065  xpmapenlem  9075  mapunen  9077  djulf1o  9827  djurf1o  9828  djur  9834  r0weon  9925  enqbreq2  10834  nqereu  10843  lterpq  10884  elreal2  11046  cnref1o  12926  ruclem6  16193  ruclem8  16195  ruclem9  16196  ruclem12  16199  eucalgval  16542  eucalginv  16544  eucalglt  16545  eucalg  16547  qnumdenbi  16705  isstruct2  17110  xpsff1o  17522  comfffval2  17658  comfeq  17663  idfucl  17839  funcpropd  17860  coapm  18029  xpccatid  18145  1stfcl  18154  2ndfcl  18155  1st2ndprf  18163  xpcpropd  18165  evlfcl  18179  hofcl  18216  hofpropd  18224  yonedalem3  18237  gsum2dlem2  19937  mdetunilem9  22595  tx1cn  23584  tx2cn  23585  txdis  23607  txlly  23611  txnlly  23612  txhaus  23622  txkgen  23627  txconn  23664  utop3cls  24226  ucnima  24255  fmucndlem  24265  psmetxrge0  24288  imasdsf1olem  24348  cnheiborlem  24931  caublcls  25286  bcthlem1  25301  bcthlem2  25302  bcthlem4  25304  bcthlem5  25305  ovolfcl  25443  ovolfioo  25444  ovolficc  25445  ovolficcss  25446  ovolfsval  25447  ovolicc2lem1  25494  ovolicc2lem5  25498  ovolfs2  25548  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2a  25559  uniioombllem2  25560  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombllem6  25565  dyadmbl  25577  fsumvma  27190  opreu2reuALT  32561  ofpreima  32753  ofpreima2  32754  elrgspnsubrunlem2  33324  erler  33341  1stmbfm  34420  2ndmbfm  34421  sibfof  34500  oddpwdcv  34515  txsconnlem  35438  mpst123  35738  bj-elid4  37498  bj-elid6  37500  poimirlem4  37959  poimirlem26  37981  poimirlem27  37982  mblfinlem1  37992  mblfinlem2  37993  ftc2nc  38037  heiborlem8  38153  dvhgrp  41567  dvhlveclem  41568  fvovco  45641  dvnprodlem1  46392  volioof  46433  fvvolioof  46435  fvvolicof  46437  etransclem44  46724  ovolval3  47093  ovolval4lem1  47095  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  smfpimbor1lem1  47244  rrx2xpref1o  49206  2oppf  49619  eloppf  49620  funcoppc5  49632  swapf2f1oa  49764  swapfida  49767  swapffunca  49771  swapfiso  49772  cofuswapf1  49781  cofuswapf2  49782  fuco2eld2  49801  fuco11b  49824  fuco11bALT  49825  fucoco2  49845  fucofunca  49847  fucolid  49848  fucorid  49849  precofvalALT  49855  reldmlan2  50104  reldmran2  50105  rellan  50110  relran  50111  ranval3  50118  ranrcl4lem  50125  ranup  50129