Theorem 1st2nd2 8010

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4598   × cxp 5639  ‘cfv 6514  1^st c1st 7969  2^nd c2nd 7970

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-1st 7971  df-2nd 7972

This theorem is referenced by:  1st2ndb  8011  xpopth  8012  eqop  8013  2nd1st  8020  1st2nd  8021  opiota  8041  fimaproj  8117  disjen  9104  xpmapenlem  9114  mapunen  9116  djulf1o  9872  djurf1o  9873  djur  9879  r0weon  9972  enqbreq2  10880  nqereu  10889  lterpq  10930  elreal2  11092  cnref1o  12951  ruclem6  16210  ruclem8  16212  ruclem9  16213  ruclem12  16216  eucalgval  16559  eucalginv  16561  eucalglt  16562  eucalg  16564  qnumdenbi  16721  isstruct2  17126  xpsff1o  17537  comfffval2  17669  comfeq  17674  idfucl  17850  funcpropd  17871  coapm  18040  xpccatid  18156  1stfcl  18165  2ndfcl  18166  1st2ndprf  18174  xpcpropd  18176  evlfcl  18190  hofcl  18227  hofpropd  18235  yonedalem3  18248  gsum2dlem2  19908  mdetunilem9  22514  tx1cn  23503  tx2cn  23504  txdis  23526  txlly  23530  txnlly  23531  txhaus  23541  txkgen  23546  txconn  23583  utop3cls  24146  ucnima  24175  fmucndlem  24185  psmetxrge0  24208  imasdsf1olem  24268  cnheiborlem  24860  caublcls  25216  bcthlem1  25231  bcthlem2  25232  bcthlem4  25234  bcthlem5  25235  ovolfcl  25374  ovolfioo  25375  ovolficc  25376  ovolficcss  25377  ovolfsval  25378  ovolicc2lem1  25425  ovolicc2lem5  25429  ovolfs2  25479  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem2a  25490  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombllem6  25496  dyadmbl  25508  fsumvma  27131  opreu2reuALT  32413  ofpreima  32596  ofpreima2  32597  elrgspnsubrunlem2  33206  erler  33223  1stmbfm  34258  2ndmbfm  34259  sibfof  34338  oddpwdcv  34353  txsconnlem  35234  mpst123  35534  bj-elid4  37163  bj-elid6  37165  poimirlem4  37625  poimirlem26  37647  poimirlem27  37648  mblfinlem1  37658  mblfinlem2  37659  ftc2nc  37703  heiborlem8  37819  dvhgrp  41108  dvhlveclem  41109  fvovco  45194  dvnprodlem1  45951  volioof  45992  fvvolioof  45994  fvvolicof  45996  etransclem44  46283  ovolval3  46652  ovolval4lem1  46654  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  smfpimbor1lem1  46803  rrx2xpref1o  48711  2oppf  49125  eloppf  49126  funcoppc5  49138  swapf2f1oa  49270  swapfida  49273  swapffunca  49277  swapfiso  49278  cofuswapf1  49287  cofuswapf2  49288  fuco2eld2  49307  fuco11b  49330  fuco11bALT  49331  fucoco2  49351  fucofunca  49353  fucolid  49354  fucorid  49355  precofvalALT  49361  reldmlan2  49610  reldmran2  49611  rellan  49616  relran  49617  ranval3  49624  ranrcl4lem  49631  ranup  49635