Theorem 1st2nd2 7960

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ⟨cop 4582   × cxp 5614  ‘cfv 6481  1^st c1st 7919  2^nd c2nd 7920

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fv 6489  df-1st 7921  df-2nd 7922

This theorem is referenced by:  1st2ndb  7961  xpopth  7962  eqop  7963  2nd1st  7970  1st2nd  7971  opiota  7991  fimaproj  8065  disjen  9047  xpmapenlem  9057  mapunen  9059  djulf1o  9805  djurf1o  9806  djur  9812  r0weon  9903  enqbreq2  10811  nqereu  10820  lterpq  10861  elreal2  11023  cnref1o  12883  ruclem6  16144  ruclem8  16146  ruclem9  16147  ruclem12  16150  eucalgval  16493  eucalginv  16495  eucalglt  16496  eucalg  16498  qnumdenbi  16655  isstruct2  17060  xpsff1o  17471  comfffval2  17607  comfeq  17612  idfucl  17788  funcpropd  17809  coapm  17978  xpccatid  18094  1stfcl  18103  2ndfcl  18104  1st2ndprf  18112  xpcpropd  18114  evlfcl  18128  hofcl  18165  hofpropd  18173  yonedalem3  18186  gsum2dlem2  19884  mdetunilem9  22536  tx1cn  23525  tx2cn  23526  txdis  23548  txlly  23552  txnlly  23553  txhaus  23563  txkgen  23568  txconn  23605  utop3cls  24167  ucnima  24196  fmucndlem  24206  psmetxrge0  24229  imasdsf1olem  24289  cnheiborlem  24881  caublcls  25237  bcthlem1  25252  bcthlem2  25253  bcthlem4  25255  bcthlem5  25256  ovolfcl  25395  ovolfioo  25396  ovolficc  25397  ovolficcss  25398  ovolfsval  25399  ovolicc2lem1  25446  ovolicc2lem5  25450  ovolfs2  25500  uniiccdif  25507  uniioovol  25508  uniiccvol  25509  uniioombllem2a  25511  uniioombllem2  25512  uniioombllem3a  25513  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  uniioombllem6  25517  dyadmbl  25529  fsumvma  27152  opreu2reuALT  32454  ofpreima  32645  ofpreima2  32646  elrgspnsubrunlem2  33213  erler  33230  1stmbfm  34271  2ndmbfm  34272  sibfof  34351  oddpwdcv  34366  txsconnlem  35282  mpst123  35582  bj-elid4  37208  bj-elid6  37210  poimirlem4  37670  poimirlem26  37692  poimirlem27  37693  mblfinlem1  37703  mblfinlem2  37704  ftc2nc  37748  heiborlem8  37864  dvhgrp  41152  dvhlveclem  41153  fvovco  45236  dvnprodlem1  45990  volioof  46031  fvvolioof  46033  fvvolicof  46035  etransclem44  46322  ovolval3  46691  ovolval4lem1  46693  ovolval5lem2  46697  ovnovollem1  46700  ovnovollem2  46701  smfpimbor1lem1  46842  rrx2xpref1o  48756  2oppf  49170  eloppf  49171  funcoppc5  49183  swapf2f1oa  49315  swapfida  49318  swapffunca  49322  swapfiso  49323  cofuswapf1  49332  cofuswapf2  49333  fuco2eld2  49352  fuco11b  49375  fuco11bALT  49376  fucoco2  49396  fucofunca  49398  fucolid  49399  fucorid  49400  precofvalALT  49406  reldmlan2  49655  reldmran2  49656  rellan  49661  relran  49662  ranval3  49669  ranrcl4lem  49676  ranup  49680