Theorem 1st2nd2 8026

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ⟨cop 4596   × cxp 5661  ‘cfv 6538  1^st c1st 7985  2^nd c2nd 7986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 7987  df-2nd 7988

This theorem is referenced by:  1st2ndb  8027  xpopth  8028  eqop  8029  2nd1st  8036  1st2nd  8037  opiota  8057  fimaproj  8132  disjen  9123  xpmapenlem  9133  mapunen  9135  djulf1o  9899  djurf1o  9900  djur  9906  r0weon  9997  enqbreq2  10906  nqereu  10915  lterpq  10956  elreal2  11118  cnref1o  13010  ruclem6  16292  ruclem8  16294  ruclem9  16295  ruclem12  16298  eucalgval  16641  eucalginv  16643  eucalglt  16644  eucalg  16646  qnumdenbi  16804  isstruct2  17210  xpsff1o  17622  comfffval2  17758  comfeq  17763  idfucl  17939  funcpropd  17960  coapm  18129  xpccatid  18245  1stfcl  18254  2ndfcl  18255  1st2ndprf  18263  xpcpropd  18265  evlfcl  18279  hofcl  18316  hofpropd  18324  yonedalem3  18337  gsum2dlem2  20042  mdetunilem9  22758  tx1cn  23747  tx2cn  23748  txdis  23770  txlly  23774  txnlly  23775  txhaus  23785  txkgen  23790  txconn  23827  utop3cls  24389  ucnima  24418  fmucndlem  24428  psmetxrge0  24451  imasdsf1olem  24511  cnheiborlem  25094  caublcls  25449  bcthlem1  25464  bcthlem2  25465  bcthlem4  25467  bcthlem5  25468  ovolfcl  25606  ovolfioo  25607  ovolficc  25608  ovolficcss  25609  ovolfsval  25610  ovolicc2lem1  25657  ovolicc2lem5  25661  ovolfs2  25711  uniiccdif  25718  uniioovol  25719  uniiccvol  25720  uniioombllem2a  25722  uniioombllem2  25723  uniioombllem3a  25724  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  uniioombllem6  25728  dyadmbl  25740  fsumvma  27355  opreu2reuALT  32801  ofpreima  32988  ofpreima2  32989  elrgspnsubrunlem2  33546  erler  33563  1stmbfm  34628  2ndmbfm  34629  sibfof  34708  oddpwdcv  34723  txsconnlem  35710  mpst123  36010  bj-elid4  37790  bj-elid6  37792  poimirlem4  38253  poimirlem26  38275  poimirlem27  38276  mblfinlem1  38286  mblfinlem2  38287  ftc2nc  38331  heiborlem8  38447  dvhgrp  41859  dvhlveclem  41860  fvovco  45891  dvnprodlem1  46640  volioof  46681  fvvolioof  46683  fvvolicof  46685  etransclem44  46972  ovolval3  47341  ovolval4lem1  47343  ovolval5lem2  47347  ovnovollem1  47350  ovnovollem2  47351  smfpimbor1lem1  47492  rrx2xpref1o  49475  2oppf  49887  eloppf  49888  funcoppc5  49900  swapf2f1oa  50032  swapfida  50035  swapffunca  50039  swapfiso  50040  cofuswapf1  50049  cofuswapf2  50050  fuco2eld2  50069  fuco11b  50092  fuco11bALT  50093  fucoco2  50113  fucofunca  50115  fucolid  50116  fucorid  50117  precofvalALT  50123  reldmlan2  50372  reldmran2  50373  rellan  50378  relran  50379  ranval3  50386  ranrcl4lem  50393  ranup  50397