Theorem 1st2nd2 7848

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ⟨cop 4569   × cxp 5583  ‘cfv 6423  1^st c1st 7807  2^nd c2nd 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7571

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3429  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-iota 6381  df-fun 6425  df-fv 6431  df-1st 7809  df-2nd 7810

This theorem is referenced by:  1st2ndb  7849  xpopth  7850  eqop  7851  2nd1st  7857  1st2nd  7858  opiota  7877  fimaproj  7952  disjen  8875  xpmapenlem  8885  mapunen  8887  djulf1o  9617  djurf1o  9618  djur  9624  r0weon  9715  enqbreq2  10623  nqereu  10632  lterpq  10673  elreal2  10835  cnref1o  12670  ruclem6  15888  ruclem8  15890  ruclem9  15891  ruclem12  15894  eucalgval  16231  eucalginv  16233  eucalglt  16234  eucalg  16236  qnumdenbi  16392  isstruct2  16794  xpsff1o  17222  comfffval2  17354  comfeq  17359  idfucl  17540  funcpropd  17560  coapm  17730  xpccatid  17849  1stfcl  17858  2ndfcl  17859  1st2ndprf  17867  xpcpropd  17870  evlfcl  17884  hofcl  17921  hofpropd  17929  yonedalem3  17942  gsum2dlem2  19516  mdetunilem9  21713  tx1cn  22704  tx2cn  22705  txdis  22727  txlly  22731  txnlly  22732  txhaus  22742  txkgen  22747  txconn  22784  utop3cls  23347  ucnima  23377  fmucndlem  23387  psmetxrge0  23410  imasdsf1olem  23470  cnheiborlem  24061  caublcls  24416  bcthlem1  24431  bcthlem2  24432  bcthlem4  24434  bcthlem5  24435  ovolfcl  24573  ovolfioo  24574  ovolficc  24575  ovolficcss  24576  ovolfsval  24577  ovolicc2lem1  24624  ovolicc2lem5  24628  ovolfs2  24678  uniiccdif  24685  uniioovol  24686  uniiccvol  24687  uniioombllem2a  24689  uniioombllem2  24690  uniioombllem3a  24691  uniioombllem3  24692  uniioombllem4  24693  uniioombllem5  24694  uniioombllem6  24695  dyadmbl  24707  fsumvma  26304  opreu2reuALT  30766  ofpreima  30944  ofpreima2  30945  1stmbfm  32169  2ndmbfm  32170  sibfof  32249  oddpwdcv  32264  txsconnlem  33144  mpst123  33444  bj-elid4  35308  bj-elid6  35310  poimirlem4  35750  poimirlem26  35772  poimirlem27  35773  mblfinlem1  35783  mblfinlem2  35784  ftc2nc  35828  heiborlem8  35945  dvhgrp  39090  dvhlveclem  39091  fvovco  42663  dvnprodlem1  43419  volioof  43460  fvvolioof  43462  fvvolicof  43464  etransclem44  43751  ovolval3  44117  ovolval4lem1  44119  ovolval5lem2  44123  ovnovollem1  44126  ovnovollem2  44127  smfpimbor1lem1  44261  rrx2xpref1o  45994