Theorem 1st2nd2 8026

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ⟨cop 4630   × cxp 5670  ‘cfv 6542  1^st c1st 7985  2^nd c2nd 7986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fv 6550  df-1st 7987  df-2nd 7988

This theorem is referenced by:  1st2ndb  8027  xpopth  8028  eqop  8029  2nd1st  8036  1st2nd  8037  opiota  8057  fimaproj  8134  disjen  9152  xpmapenlem  9162  mapunen  9164  djulf1o  9929  djurf1o  9930  djur  9936  r0weon  10029  enqbreq2  10937  nqereu  10946  lterpq  10987  elreal2  11149  cnref1o  12993  ruclem6  16205  ruclem8  16207  ruclem9  16208  ruclem12  16211  eucalgval  16546  eucalginv  16548  eucalglt  16549  eucalg  16551  qnumdenbi  16709  isstruct2  17111  xpsff1o  17542  comfffval2  17674  comfeq  17679  idfucl  17860  funcpropd  17882  coapm  18053  xpccatid  18172  1stfcl  18181  2ndfcl  18182  1st2ndprf  18190  xpcpropd  18193  evlfcl  18207  hofcl  18244  hofpropd  18252  yonedalem3  18265  gsum2dlem2  19919  mdetunilem9  22515  tx1cn  23506  tx2cn  23507  txdis  23529  txlly  23533  txnlly  23534  txhaus  23544  txkgen  23549  txconn  23586  utop3cls  24149  ucnima  24179  fmucndlem  24189  psmetxrge0  24212  imasdsf1olem  24272  cnheiborlem  24873  caublcls  25230  bcthlem1  25245  bcthlem2  25246  bcthlem4  25248  bcthlem5  25249  ovolfcl  25388  ovolfioo  25389  ovolficc  25390  ovolficcss  25391  ovolfsval  25392  ovolicc2lem1  25439  ovolicc2lem5  25443  ovolfs2  25493  uniiccdif  25500  uniioovol  25501  uniiccvol  25502  uniioombllem2a  25504  uniioombllem2  25505  uniioombllem3a  25506  uniioombllem3  25507  uniioombllem4  25508  uniioombllem5  25509  uniioombllem6  25510  dyadmbl  25522  fsumvma  27139  opreu2reuALT  32268  ofpreima  32444  ofpreima2  32445  erler  32973  1stmbfm  33870  2ndmbfm  33871  sibfof  33950  oddpwdcv  33965  txsconnlem  34840  mpst123  35140  bj-elid4  36637  bj-elid6  36639  poimirlem4  37086  poimirlem26  37108  poimirlem27  37109  mblfinlem1  37119  mblfinlem2  37120  ftc2nc  37164  heiborlem8  37280  dvhgrp  40569  dvhlveclem  40570  fvovco  44538  dvnprodlem1  45306  volioof  45347  fvvolioof  45349  fvvolicof  45351  etransclem44  45638  ovolval3  46007  ovolval4lem1  46009  ovolval5lem2  46013  ovnovollem1  46016  ovnovollem2  46017  smfpimbor1lem1  46158  rrx2xpref1o  47763