Theorem 1st2nd2 8029

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4593   × cxp 5657  ‘cfv 6537  1^st c1st 7988  2^nd c2nd 7989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fv 6545  df-1st 7990  df-2nd 7991

This theorem is used by:  1st2ndb  8030  xpopth  8031  eqop  8032  2nd1st  8039  1st2nd  8040  opiota  8060  fimaproj  8137  disjen  9136  xpmapenlem  9146  mapunen  9148  djulf1o  9921  djurf1o  9922  djur  9928  r0weon  10019  enqbreq2  10933  nqereu  10942  lterpq  10983  elreal2  11145  cnref1o  13039  ruclem6  16329  ruclem8  16331  ruclem9  16332  ruclem12  16335  eucalgval  16678  eucalginv  16680  eucalglt  16681  eucalg  16683  qnumdenbi  16841  isstruct2  17247  xpsff1o  17659  comfffval2  17795  comfeq  17800  idfucl  17976  funcpropd  17997  coapm  18166  xpccatid  18282  1stfcl  18291  2ndfcl  18292  1st2ndprf  18300  xpcpropd  18302  evlfcl  18316  hofcl  18353  hofpropd  18361  yonedalem3  18374  gsum2dlem2  20104  mdetunilem9  22848  tx1cn  23841  tx2cn  23842  txdis  23864  txlly  23868  txnlly  23869  txhaus  23879  txkgen  23884  txconn  23921  utop3cls  24483  ucnima  24512  fmucndlem  24522  psmetxrge0  24545  imasdsf1olem  24605  cnheiborlem  25188  caublcls  25543  bcthlem1  25558  bcthlem2  25559  bcthlem4  25561  bcthlem5  25562  ovolfcl  25700  ovolfioo  25701  ovolficc  25702  ovolficcss  25703  ovolfsval  25704  ovolicc2lem1  25751  ovolicc2lem5  25755  ovolfs2  25805  uniiccdif  25812  uniioovol  25813  uniiccvol  25814  uniioombllem2a  25816  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  uniioombllem6  25822  dyadmbl  25834  fsumvma  27457  opreu2reuALT  32960  ofpreima  33146  ofpreima2  33147  elrgspnsubrunlem2  33696  erler  33713  1stmbfm  34779  2ndmbfm  34780  sibfof  34859  oddpwdcv  34874  txsconnlem  35827  mpst123  36127  bj-elid4  37928  bj-elid6  37930  poimirlem4  38381  poimirlem26  38403  poimirlem27  38404  mblfinlem1  38414  mblfinlem2  38415  ftc2nc  38459  heiborlem8  38576  dvhgrp  41988  dvhlveclem  41989  fvovco  46033  dvnprodlem1  46782  volioof  46823  fvvolioof  46825  fvvolicof  46827  etransclem44  47114  ovolval3  47483  ovolval4lem1  47485  ovolval5lem2  47489  ovnovollem1  47492  ovnovollem2  47493  smfpimbor1lem1  47634  rrx2xpref1o  49656  2oppf  50066  eloppf  50067  funcoppc5  50079  swapf2f1oa  50211  swapfida  50214  swapffunca  50218  swapfiso  50219  cofuswapf1  50228  cofuswapf2  50229  fuco2eld2  50248  fuco11b  50271  fuco11bALT  50272  fucoco2  50292  fucofunca  50294  fucolid  50295  fucorid  50296  precofvalALT  50302  reldmlan2  50551  reldmran2  50552  rellan  50557  relran  50558  ranval3  50565  ranrcl4lem  50572  ranup  50576