Theorem 1st2nd2 8005

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ⟨cop 4587   × cxp 5643  ‘cfv 6517  1^st c1st 7964  2^nd c2nd 7965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fv 6525  df-1st 7966  df-2nd 7967

This theorem is referenced by:  1st2ndb  8006  xpopth  8007  eqop  8008  2nd1st  8015  1st2nd  8016  opiota  8036  fimaproj  8110  disjen  9102  xpmapenlem  9112  mapunen  9114  djulf1o  9867  djurf1o  9868  djur  9874  r0weon  9965  enqbreq2  10875  nqereu  10884  lterpq  10925  elreal2  11087  cnref1o  12983  ruclem6  16250  ruclem8  16252  ruclem9  16253  ruclem12  16256  eucalgval  16599  eucalginv  16601  eucalglt  16602  eucalg  16604  qnumdenbi  16762  isstruct2  17168  xpsff1o  17580  comfffval2  17716  comfeq  17721  idfucl  17897  funcpropd  17918  coapm  18087  xpccatid  18203  1stfcl  18212  2ndfcl  18213  1st2ndprf  18221  xpcpropd  18223  evlfcl  18237  hofcl  18274  hofpropd  18282  yonedalem3  18295  gsum2dlem2  19994  mdetunilem9  22660  tx1cn  23649  tx2cn  23650  txdis  23672  txlly  23676  txnlly  23677  txhaus  23687  txkgen  23692  txconn  23729  utop3cls  24291  ucnima  24320  fmucndlem  24330  psmetxrge0  24353  imasdsf1olem  24413  cnheiborlem  24996  caublcls  25351  bcthlem1  25366  bcthlem2  25367  bcthlem4  25369  bcthlem5  25370  ovolfcl  25508  ovolfioo  25509  ovolficc  25510  ovolficcss  25511  ovolfsval  25512  ovolicc2lem1  25559  ovolicc2lem5  25563  ovolfs2  25613  uniiccdif  25620  uniioovol  25621  uniiccvol  25622  uniioombllem2a  25624  uniioombllem2  25625  uniioombllem3a  25626  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  uniioombllem6  25630  dyadmbl  25642  fsumvma  27254  opreu2reuALT  32624  ofpreima  32817  ofpreima2  32818  elrgspnsubrunlem2  33390  erler  33407  1stmbfm  34518  2ndmbfm  34519  sibfof  34598  oddpwdcv  34613  txsconnlem  35554  mpst123  35854  bj-elid4  37624  bj-elid6  37626  poimirlem4  38087  poimirlem26  38109  poimirlem27  38110  mblfinlem1  38120  mblfinlem2  38121  ftc2nc  38165  heiborlem8  38281  dvhgrp  41695  dvhlveclem  41696  fvovco  45735  dvnprodlem1  46484  volioof  46525  fvvolioof  46527  fvvolicof  46529  etransclem44  46816  ovolval3  47185  ovolval4lem1  47187  ovolval5lem2  47191  ovnovollem1  47194  ovnovollem2  47195  smfpimbor1lem1  47336  rrx2xpref1o  49304  2oppf  49717  eloppf  49718  funcoppc5  49730  swapf2f1oa  49862  swapfida  49865  swapffunca  49869  swapfiso  49870  cofuswapf1  49879  cofuswapf2  49880  fuco2eld2  49899  fuco11b  49922  fuco11bALT  49923  fucoco2  49943  fucofunca  49945  fucolid  49946  fucorid  49947  precofvalALT  49953  reldmlan2  50202  reldmran2  50203  rellan  50208  relran  50209  ranval3  50216  ranrcl4lem  50223  ranup  50227