Theorem 1st2nd2 8064

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 8059	. 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 2147  ⟨cop 4838   × cxp 5653  ‘cfv 6558  1^st c1st 8023  2^nd c2nd 8024

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fv 6566  df-1st 8025  df-2nd 8026

This theorem is used by:  1st2ndb  8065  xpopth  8066  eqop  8067  2nd1st  8073  1st2nd  8074  opiota  8095  fimaproj  8179  disjen  9181  xpmapenlem  9191  mapunen  9193  djulf1o  10020  djurf1o  10021  djur  10027  r0weon  10118  enqbreq2  11032  nqereu  11041  lterpq  11082  elreal2  11244  cnref1o  13140  ruclem6  16432  ruclem8  16434  ruclem9  16435  ruclem12  16438  eucalgval  16786  eucalginv  16788  eucalglt  16789  eucalg  16791  qnumdenbi  16949  isstruct2  17356  xpsff1o  17768  comfffval2  17904  comfeq  17909  idfucl  18085  funcpropd  18106  coapm  18275  xpccatid  18391  1stfcl  18400  2ndfcl  18401  1st2ndprf  18409  xpcpropd  18411  evlfcl  18425  hofcl  18462  hofpropd  18470  yonedalem3  18483  gsum2dlem2  20215  mdetunilem9  22965  tx1cn  23958  tx2cn  23959  txdis  23981  txlly  23985  txnlly  23986  txhaus  23996  txkgen  24001  txconn  24038  utop3cls  24600  ucnima  24629  fmucndlem  24639  psmetxrge0  24662  imasdsf1olem  24722  cnheiborlem  25305  caublcls  25660  bcthlem1  25675  bcthlem2  25676  bcthlem4  25678  bcthlem5  25679  ovolfcl  25817  ovolfioo  25818  ovolficc  25819  ovolficcss  25820  ovolfsval  25821  ovolicc2lem1  25868  ovolicc2lem5  25872  ovolfs2  25922  uniiccdif  25929  uniioovol  25930  uniiccvol  25931  uniioombllem2a  25933  uniioombllem2  25934  uniioombllem3a  25935  uniioombllem3  25936  uniioombllem4  25937  uniioombllem5  25938  uniioombllem6  25939  dyadmbl  25951  fsumvma  27570  opreu2reuALT  33145  ofpreima  33331  ofpreima2  33332  elrgspnsubrunlem2  33879  erler  33896  1stmbfm  34962  2ndmbfm  34963  sibfof  35042  oddpwdcv  35057  ot1st2nd  35795  txsconnlem  36172  mpst123  36472  bj-elid4  38281  bj-elid6  38283  poimirlem4  38734  poimirlem26  38756  poimirlem27  38757  mblfinlem1  38767  mblfinlem2  38768  ftc2nc  38812  heiborlem8  38944  dvhgrp  42356  dvhlveclem  42357  fvovco  46413  dvnprodlem1  47161  volioof  47202  fvvolioof  47204  fvvolicof  47206  etransclem44  47493  ovolval3  47862  ovolval4lem1  47864  ovolval5lem2  47868  ovnovollem1  47871  ovnovollem2  47872  smfpimbor1lem1  48013  2oppf  50453  eloppf  50454  funcoppc5  50466  swapf2f1oa  50604  swapfida  50607  swapffunca  50611  swapfiso  50612  cofuswapf1  50621  cofuswapf2  50622  fuco2eld2  50641  fuco11b  50664  fuco11bALT  50665  fucoco2  50685  fucofunca  50687  fucolid  50688  fucorid  50689  precofvalALT  50708  reldmlan2  51005  reldmran2  51006  rellan  51011  relran  51012  ranval3  51019  ranrcl4lem  51026  ranup  51030