Theorem 1st2nd2 7710

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ⟨cop 4531   × cxp 5517  ‘cfv 6324  1^st c1st 7669  2^nd c2nd 7670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fv 6332  df-1st 7671  df-2nd 7672

This theorem is referenced by:  1st2ndb  7711  xpopth  7712  eqop  7713  2nd1st  7719  1st2nd  7720  opiota  7739  fimaproj  7812  disjen  8658  xpmapenlem  8668  mapunen  8670  djulf1o  9325  djurf1o  9326  djur  9332  r0weon  9423  enqbreq2  10331  nqereu  10340  lterpq  10381  elreal2  10543  cnref1o  12372  ruclem6  15580  ruclem8  15582  ruclem9  15583  ruclem12  15586  eucalgval  15916  eucalginv  15918  eucalglt  15919  eucalg  15921  qnumdenbi  16074  isstruct2  16485  xpsff1o  16832  comfffval2  16963  comfeq  16968  idfucl  17143  funcpropd  17162  coapm  17323  xpccatid  17430  1stfcl  17439  2ndfcl  17440  1st2ndprf  17448  xpcpropd  17450  evlfcl  17464  hofcl  17501  hofpropd  17509  yonedalem3  17522  gsum2dlem2  19084  mdetunilem9  21225  tx1cn  22214  tx2cn  22215  txdis  22237  txlly  22241  txnlly  22242  txhaus  22252  txkgen  22257  txconn  22294  utop3cls  22857  ucnima  22887  fmucndlem  22897  psmetxrge0  22920  imasdsf1olem  22980  cnheiborlem  23559  caublcls  23913  bcthlem1  23928  bcthlem2  23929  bcthlem4  23931  bcthlem5  23932  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  25797  opreu2reuALT  30247  ofpreima  30428  ofpreima2  30429  1stmbfm  31628  2ndmbfm  31629  sibfof  31708  oddpwdcv  31723  txsconnlem  32600  mpst123  32900  bj-elid4  34583  bj-elid6  34585  poimirlem4  35061  poimirlem26  35083  poimirlem27  35084  mblfinlem1  35094  mblfinlem2  35095  ftc2nc  35139  heiborlem8  35256  dvhgrp  38403  dvhlveclem  38404  fvovco  41821  dvnprodlem1  42588  volioof  42629  fvvolioof  42631  fvvolicof  42633  etransclem44  42920  ovolval3  43286  ovolval4lem1  43288  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  smfpimbor1lem1  43430  rrx2xpref1o  45132