Theorem 1st2nd2 8027

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4607   × cxp 5652  ‘cfv 6531  1^st c1st 7986  2^nd c2nd 7987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fv 6539  df-1st 7988  df-2nd 7989

This theorem is referenced by:  1st2ndb  8028  xpopth  8029  eqop  8030  2nd1st  8037  1st2nd  8038  opiota  8058  fimaproj  8134  disjen  9148  xpmapenlem  9158  mapunen  9160  djulf1o  9926  djurf1o  9927  djur  9933  r0weon  10026  enqbreq2  10934  nqereu  10943  lterpq  10984  elreal2  11146  cnref1o  13001  ruclem6  16253  ruclem8  16255  ruclem9  16256  ruclem12  16259  eucalgval  16601  eucalginv  16603  eucalglt  16604  eucalg  16606  qnumdenbi  16763  isstruct2  17168  xpsff1o  17581  comfffval2  17713  comfeq  17718  idfucl  17894  funcpropd  17915  coapm  18084  xpccatid  18200  1stfcl  18209  2ndfcl  18210  1st2ndprf  18218  xpcpropd  18220  evlfcl  18234  hofcl  18271  hofpropd  18279  yonedalem3  18292  gsum2dlem2  19952  mdetunilem9  22558  tx1cn  23547  tx2cn  23548  txdis  23570  txlly  23574  txnlly  23575  txhaus  23585  txkgen  23590  txconn  23627  utop3cls  24190  ucnima  24219  fmucndlem  24229  psmetxrge0  24252  imasdsf1olem  24312  cnheiborlem  24904  caublcls  25261  bcthlem1  25276  bcthlem2  25277  bcthlem4  25279  bcthlem5  25280  ovolfcl  25419  ovolfioo  25420  ovolficc  25421  ovolficcss  25422  ovolfsval  25423  ovolicc2lem1  25470  ovolicc2lem5  25474  ovolfs2  25524  uniiccdif  25531  uniioovol  25532  uniiccvol  25533  uniioombllem2a  25535  uniioombllem2  25536  uniioombllem3a  25537  uniioombllem3  25538  uniioombllem4  25539  uniioombllem5  25540  uniioombllem6  25541  dyadmbl  25553  fsumvma  27176  opreu2reuALT  32458  ofpreima  32643  ofpreima2  32644  elrgspnsubrunlem2  33243  erler  33260  1stmbfm  34292  2ndmbfm  34293  sibfof  34372  oddpwdcv  34387  txsconnlem  35262  mpst123  35562  bj-elid4  37186  bj-elid6  37188  poimirlem4  37648  poimirlem26  37670  poimirlem27  37671  mblfinlem1  37681  mblfinlem2  37682  ftc2nc  37726  heiborlem8  37842  dvhgrp  41126  dvhlveclem  41127  fvovco  45217  dvnprodlem1  45975  volioof  46016  fvvolioof  46018  fvvolicof  46020  etransclem44  46307  ovolval3  46676  ovolval4lem1  46678  ovolval5lem2  46682  ovnovollem1  46685  ovnovollem2  46686  smfpimbor1lem1  46827  rrx2xpref1o  48698  2oppf  49080  funcoppc5  49088  swapf2f1oa  49194  swapfida  49197  swapffunca  49201  swapfiso  49202  cofuswapf1  49205  cofuswapf2  49206  fuco2eld2  49225  fuco11b  49248  fuco11bALT  49249  fucoco2  49269  fucofunca  49271  fucolid  49272  fucorid  49273  precofvalALT  49279  reldmlan2  49492  reldmran2  49493  rellan  49498  relran  49499  ranrcl4lem  49512  ranup  49516