Theorem 1st2nd2 7728

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ⟨cop 4573   × cxp 5553  ‘cfv 6355  1^st c1st 7687  2^nd c2nd 7688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fv 6363  df-1st 7689  df-2nd 7690

This theorem is referenced by:  1st2ndb  7729  xpopth  7730  eqop  7731  2nd1st  7737  1st2nd  7738  opiota  7757  fimaproj  7829  disjen  8674  xpmapenlem  8684  mapunen  8686  djulf1o  9341  djurf1o  9342  djur  9348  r0weon  9438  enqbreq2  10342  nqereu  10351  lterpq  10392  elreal2  10554  cnref1o  12385  ruclem6  15588  ruclem8  15590  ruclem9  15591  ruclem12  15594  eucalgval  15926  eucalginv  15928  eucalglt  15929  eucalg  15931  qnumdenbi  16084  isstruct2  16493  xpsff1o  16840  comfffval2  16971  comfeq  16976  idfucl  17151  funcpropd  17170  coapm  17331  xpccatid  17438  1stfcl  17447  2ndfcl  17448  1st2ndprf  17456  xpcpropd  17458  evlfcl  17472  hofcl  17509  hofpropd  17517  yonedalem3  17530  gsum2dlem2  19091  mdetunilem9  21229  tx1cn  22217  tx2cn  22218  txdis  22240  txlly  22244  txnlly  22245  txhaus  22255  txkgen  22260  txconn  22297  utop3cls  22860  ucnima  22890  fmucndlem  22900  psmetxrge0  22923  imasdsf1olem  22983  cnheiborlem  23558  caublcls  23912  bcthlem1  23927  bcthlem2  23928  bcthlem4  23930  bcthlem5  23931  ovolfcl  24067  ovolfioo  24068  ovolficc  24069  ovolficcss  24070  ovolfsval  24071  ovolicc2lem1  24118  ovolicc2lem5  24122  ovolfs2  24172  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2a  24183  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombllem6  24189  dyadmbl  24201  fsumvma  25789  opreu2reuALT  30240  ofpreima  30410  ofpreima2  30411  1stmbfm  31518  2ndmbfm  31519  sibfof  31598  oddpwdcv  31613  txsconnlem  32487  mpst123  32787  bj-elid4  34463  bj-elid6  34465  poimirlem4  34911  poimirlem26  34933  poimirlem27  34934  mblfinlem1  34944  mblfinlem2  34945  ftc2nc  34991  heiborlem8  35111  dvhgrp  38258  dvhlveclem  38259  fvovco  41475  dvnprodlem1  42251  volioof  42292  fvvolioof  42294  fvvolicof  42296  etransclem44  42583  ovolval3  42949  ovolval4lem1  42951  ovolval5lem2  42955  ovnovollem1  42958  ovnovollem2  42959  smfpimbor1lem1  43093  rrx2xpref1o  44725