Theorem 1st2nd2 8018

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  ⟨cop 4634   × cxp 5674  ‘cfv 6543  1^st c1st 7977  2^nd c2nd 7978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fv 6551  df-1st 7979  df-2nd 7980

This theorem is referenced by:  1st2ndb  8019  xpopth  8020  eqop  8021  2nd1st  8028  1st2nd  8029  opiota  8049  fimaproj  8126  disjen  9140  xpmapenlem  9150  mapunen  9152  djulf1o  9913  djurf1o  9914  djur  9920  r0weon  10013  enqbreq2  10921  nqereu  10930  lterpq  10971  elreal2  11133  cnref1o  12976  ruclem6  16185  ruclem8  16187  ruclem9  16188  ruclem12  16191  eucalgval  16526  eucalginv  16528  eucalglt  16529  eucalg  16531  qnumdenbi  16687  isstruct2  17089  xpsff1o  17520  comfffval2  17652  comfeq  17657  idfucl  17838  funcpropd  17860  coapm  18031  xpccatid  18150  1stfcl  18159  2ndfcl  18160  1st2ndprf  18168  xpcpropd  18171  evlfcl  18185  hofcl  18222  hofpropd  18230  yonedalem3  18243  gsum2dlem2  19887  mdetunilem9  22443  tx1cn  23434  tx2cn  23435  txdis  23457  txlly  23461  txnlly  23462  txhaus  23472  txkgen  23477  txconn  23514  utop3cls  24077  ucnima  24107  fmucndlem  24117  psmetxrge0  24140  imasdsf1olem  24200  cnheiborlem  24801  caublcls  25158  bcthlem1  25173  bcthlem2  25174  bcthlem4  25176  bcthlem5  25177  ovolfcl  25316  ovolfioo  25317  ovolficc  25318  ovolficcss  25319  ovolfsval  25320  ovolicc2lem1  25367  ovolicc2lem5  25371  ovolfs2  25421  uniiccdif  25428  uniioovol  25429  uniiccvol  25430  uniioombllem2a  25432  uniioombllem2  25433  uniioombllem3a  25434  uniioombllem3  25435  uniioombllem4  25436  uniioombllem5  25437  uniioombllem6  25438  dyadmbl  25450  fsumvma  27061  opreu2reuALT  32152  ofpreima  32325  ofpreima2  32326  1stmbfm  33725  2ndmbfm  33726  sibfof  33805  oddpwdcv  33820  txsconnlem  34697  mpst123  34997  bj-elid4  36516  bj-elid6  36518  poimirlem4  36959  poimirlem26  36981  poimirlem27  36982  mblfinlem1  36992  mblfinlem2  36993  ftc2nc  37037  heiborlem8  37153  dvhgrp  40445  dvhlveclem  40446  fvovco  44354  dvnprodlem1  45124  volioof  45165  fvvolioof  45167  fvvolicof  45169  etransclem44  45456  ovolval3  45825  ovolval4lem1  45827  ovolval5lem2  45831  ovnovollem1  45834  ovnovollem2  45835  smfpimbor1lem1  45976  rrx2xpref1o  47569