Theorem 1st2nd2 7731

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ⟨cop 4576   × cxp 5556  ‘cfv 6358  1^st c1st 7690  2^nd c2nd 7691

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-iota 6317  df-fun 6360  df-fv 6366  df-1st 7692  df-2nd 7693

This theorem is referenced by:  1st2ndb  7732  xpopth  7733  eqop  7734  2nd1st  7740  1st2nd  7741  opiota  7760  fimaproj  7832  disjen  8677  xpmapenlem  8687  mapunen  8689  djulf1o  9344  djurf1o  9345  djur  9351  r0weon  9441  enqbreq2  10345  nqereu  10354  lterpq  10395  elreal2  10557  cnref1o  12387  ruclem6  15591  ruclem8  15593  ruclem9  15594  ruclem12  15597  eucalgval  15929  eucalginv  15931  eucalglt  15932  eucalg  15934  qnumdenbi  16087  isstruct2  16496  xpsff1o  16843  comfffval2  16974  comfeq  16979  idfucl  17154  funcpropd  17173  coapm  17334  xpccatid  17441  1stfcl  17450  2ndfcl  17451  1st2ndprf  17459  xpcpropd  17461  evlfcl  17475  hofcl  17512  hofpropd  17520  yonedalem3  17533  gsum2dlem2  19094  mdetunilem9  21232  tx1cn  22220  tx2cn  22221  txdis  22243  txlly  22247  txnlly  22248  txhaus  22258  txkgen  22263  txconn  22300  utop3cls  22863  ucnima  22893  fmucndlem  22903  psmetxrge0  22926  imasdsf1olem  22986  cnheiborlem  23561  caublcls  23915  bcthlem1  23930  bcthlem2  23931  bcthlem4  23933  bcthlem5  23934  ovolfcl  24070  ovolfioo  24071  ovolficc  24072  ovolficcss  24073  ovolfsval  24074  ovolicc2lem1  24121  ovolicc2lem5  24125  ovolfs2  24175  uniiccdif  24182  uniioovol  24183  uniiccvol  24184  uniioombllem2a  24186  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem5  24191  uniioombllem6  24192  dyadmbl  24204  fsumvma  25792  opreu2reuALT  30243  ofpreima  30413  ofpreima2  30414  1stmbfm  31522  2ndmbfm  31523  sibfof  31602  oddpwdcv  31617  txsconnlem  32491  mpst123  32791  bj-elid4  34464  bj-elid6  34466  poimirlem4  34900  poimirlem26  34922  poimirlem27  34923  mblfinlem1  34933  mblfinlem2  34934  ftc2nc  34980  heiborlem8  35100  dvhgrp  38247  dvhlveclem  38248  fvovco  41461  dvnprodlem1  42237  volioof  42279  fvvolioof  42281  fvvolicof  42283  etransclem44  42570  ovolval3  42936  ovolval4lem1  42938  ovolval5lem2  42942  ovnovollem1  42945  ovnovollem2  42946  smfpimbor1lem1  43080  rrx2xpref1o  44712