Theorem 1st2nd2 8034

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 8029	. 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 2146  ⟨cop 4600   × cxp 5664  ‘cfv 6543  1^st c1st 7993  2^nd c2nd 7994

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fv 6551  df-1st 7995  df-2nd 7996

This theorem is used by:  1st2ndb  8035  xpopth  8036  eqop  8037  2nd1st  8044  1st2nd  8045  opiota  8065  fimaproj  8140  disjen  9132  xpmapenlem  9142  mapunen  9144  djulf1o  9917  djurf1o  9918  djur  9924  r0weon  10015  enqbreq2  10923  nqereu  10932  lterpq  10973  elreal2  11135  cnref1o  13027  ruclem6  16316  ruclem8  16318  ruclem9  16319  ruclem12  16322  eucalgval  16665  eucalginv  16667  eucalglt  16668  eucalg  16670  qnumdenbi  16828  isstruct2  17234  xpsff1o  17646  comfffval2  17782  comfeq  17787  idfucl  17963  funcpropd  17984  coapm  18153  xpccatid  18269  1stfcl  18278  2ndfcl  18279  1st2ndprf  18287  xpcpropd  18289  evlfcl  18303  hofcl  18340  hofpropd  18348  yonedalem3  18361  gsum2dlem2  20072  mdetunilem9  22814  tx1cn  23803  tx2cn  23804  txdis  23826  txlly  23830  txnlly  23831  txhaus  23841  txkgen  23846  txconn  23883  utop3cls  24445  ucnima  24474  fmucndlem  24484  psmetxrge0  24507  imasdsf1olem  24567  cnheiborlem  25150  caublcls  25505  bcthlem1  25520  bcthlem2  25521  bcthlem4  25523  bcthlem5  25524  ovolfcl  25662  ovolfioo  25663  ovolficc  25664  ovolficcss  25665  ovolfsval  25666  ovolicc2lem1  25713  ovolicc2lem5  25717  ovolfs2  25767  uniiccdif  25774  uniioovol  25775  uniiccvol  25776  uniioombllem2a  25778  uniioombllem2  25779  uniioombllem3a  25780  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  uniioombllem6  25784  dyadmbl  25796  fsumvma  27414  opreu2reuALT  32860  ofpreima  33047  ofpreima2  33048  elrgspnsubrunlem2  33599  erler  33616  1stmbfm  34681  2ndmbfm  34682  sibfof  34761  oddpwdcv  34776  txsconnlem  35752  mpst123  36052  bj-elid4  37852  bj-elid6  37854  poimirlem4  38315  poimirlem26  38337  poimirlem27  38338  mblfinlem1  38348  mblfinlem2  38349  ftc2nc  38393  heiborlem8  38509  dvhgrp  41921  dvhlveclem  41922  fvovco  45951  dvnprodlem1  46700  volioof  46741  fvvolioof  46743  fvvolicof  46745  etransclem44  47032  ovolval3  47401  ovolval4lem1  47403  ovolval5lem2  47407  ovnovollem1  47410  ovnovollem2  47411  smfpimbor1lem1  47552  rrx2xpref1o  49538  2oppf  49950  eloppf  49951  funcoppc5  49963  swapf2f1oa  50095  swapfida  50098  swapffunca  50102  swapfiso  50103  cofuswapf1  50112  cofuswapf2  50113  fuco2eld2  50132  fuco11b  50155  fuco11bALT  50156  fucoco2  50176  fucofunca  50178  fucolid  50179  fucorid  50180  precofvalALT  50186  reldmlan2  50435  reldmran2  50436  rellan  50441  relran  50442  ranval3  50449  ranrcl4lem  50456  ranup  50460