Theorem 1st2nd2 7965

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ⟨cop 4597   × cxp 5636  ‘cfv 6501  1^st c1st 7924  2^nd c2nd 7925

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fv 6509  df-1st 7926  df-2nd 7927

This theorem is referenced by:  1st2ndb  7966  xpopth  7967  eqop  7968  2nd1st  7975  1st2nd  7976  opiota  7996  fimaproj  8072  disjen  9085  xpmapenlem  9095  mapunen  9097  djulf1o  9857  djurf1o  9858  djur  9864  r0weon  9957  enqbreq2  10865  nqereu  10874  lterpq  10915  elreal2  11077  cnref1o  12919  ruclem6  16128  ruclem8  16130  ruclem9  16131  ruclem12  16134  eucalgval  16469  eucalginv  16471  eucalglt  16472  eucalg  16474  qnumdenbi  16630  isstruct2  17032  xpsff1o  17463  comfffval2  17595  comfeq  17600  idfucl  17781  funcpropd  17801  coapm  17971  xpccatid  18090  1stfcl  18099  2ndfcl  18100  1st2ndprf  18108  xpcpropd  18111  evlfcl  18125  hofcl  18162  hofpropd  18170  yonedalem3  18183  gsum2dlem2  19762  mdetunilem9  22006  tx1cn  22997  tx2cn  22998  txdis  23020  txlly  23024  txnlly  23025  txhaus  23035  txkgen  23040  txconn  23077  utop3cls  23640  ucnima  23670  fmucndlem  23680  psmetxrge0  23703  imasdsf1olem  23763  cnheiborlem  24354  caublcls  24710  bcthlem1  24725  bcthlem2  24726  bcthlem4  24728  bcthlem5  24729  ovolfcl  24867  ovolfioo  24868  ovolficc  24869  ovolficcss  24870  ovolfsval  24871  ovolicc2lem1  24918  ovolicc2lem5  24922  ovolfs2  24972  uniiccdif  24979  uniioovol  24980  uniiccvol  24981  uniioombllem2a  24983  uniioombllem2  24984  uniioombllem3a  24985  uniioombllem3  24986  uniioombllem4  24987  uniioombllem5  24988  uniioombllem6  24989  dyadmbl  25001  fsumvma  26598  opreu2reuALT  31469  ofpreima  31648  ofpreima2  31649  1stmbfm  32949  2ndmbfm  32950  sibfof  33029  oddpwdcv  33044  txsconnlem  33921  mpst123  34221  bj-elid4  35712  bj-elid6  35714  poimirlem4  36155  poimirlem26  36177  poimirlem27  36178  mblfinlem1  36188  mblfinlem2  36189  ftc2nc  36233  heiborlem8  36350  dvhgrp  39643  dvhlveclem  39644  fvovco  43535  dvnprodlem1  44307  volioof  44348  fvvolioof  44350  fvvolicof  44352  etransclem44  44639  ovolval3  45008  ovolval4lem1  45010  ovolval5lem2  45014  ovnovollem1  45017  ovnovollem2  45018  smfpimbor1lem1  45159  rrx2xpref1o  46924