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 4590   × cxp 5649  ‘cfv 6531  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 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fv 6539  df-1st 7990  df-2nd 7991

This theorem is used by:  1st2ndb  8030  xpopth  8031  eqop  8032  2nd1st  8038  1st2nd  8039  opiota  8059  fimaproj  8136  disjen  9137  xpmapenlem  9147  mapunen  9149  djulf1o  9974  djurf1o  9975  djur  9981  r0weon  10072  enqbreq2  10986  nqereu  10995  lterpq  11036  elreal2  11198  cnref1o  13094  ruclem6  16383  ruclem8  16385  ruclem9  16386  ruclem12  16389  eucalgval  16737  eucalginv  16739  eucalglt  16740  eucalg  16742  qnumdenbi  16900  isstruct2  17307  xpsff1o  17719  comfffval2  17855  comfeq  17860  idfucl  18036  funcpropd  18057  coapm  18226  xpccatid  18342  1stfcl  18351  2ndfcl  18352  1st2ndprf  18360  xpcpropd  18362  evlfcl  18376  hofcl  18413  hofpropd  18421  yonedalem3  18434  gsum2dlem2  20165  mdetunilem9  22915  tx1cn  23908  tx2cn  23909  txdis  23931  txlly  23935  txnlly  23936  txhaus  23946  txkgen  23951  txconn  23988  utop3cls  24550  ucnima  24579  fmucndlem  24589  psmetxrge0  24612  imasdsf1olem  24672  cnheiborlem  25255  caublcls  25610  bcthlem1  25625  bcthlem2  25626  bcthlem4  25628  bcthlem5  25629  ovolfcl  25767  ovolfioo  25768  ovolficc  25769  ovolficcss  25770  ovolfsval  25771  ovolicc2lem1  25818  ovolicc2lem5  25822  ovolfs2  25872  uniiccdif  25879  uniioovol  25880  uniiccvol  25881  uniioombllem2a  25883  uniioombllem2  25884  uniioombllem3a  25885  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  uniioombllem6  25889  dyadmbl  25901  fsumvma  27522  opreu2reuALT  33055  ofpreima  33241  ofpreima2  33242  elrgspnsubrunlem2  33791  erler  33808  1stmbfm  34875  2ndmbfm  34876  sibfof  34955  oddpwdcv  34970  txsconnlem  35974  mpst123  36274  bj-elid4  38057  bj-elid6  38059  poimirlem4  38510  poimirlem26  38532  poimirlem27  38533  mblfinlem1  38543  mblfinlem2  38544  ftc2nc  38588  heiborlem8  38720  dvhgrp  42132  dvhlveclem  42133  fvovco  46151  dvnprodlem1  46900  volioof  46941  fvvolioof  46943  fvvolicof  46945  etransclem44  47232  ovolval3  47601  ovolval4lem1  47603  ovolval5lem2  47607  ovnovollem1  47610  ovnovollem2  47611  smfpimbor1lem1  47752  rrx2xpref1o  49774  2oppf  50184  eloppf  50185  funcoppc5  50197  swapf2f1oa  50329  swapfida  50332  swapffunca  50336  swapfiso  50337  cofuswapf1  50346  cofuswapf2  50347  fuco2eld2  50366  fuco11b  50389  fuco11bALT  50390  fucoco2  50410  fucofunca  50412  fucolid  50413  fucorid  50414  precofvalALT  50420  reldmlan2  50669  reldmran2  50670  rellan  50675  relran  50676  ranval3  50683  ranrcl4lem  50690  ranup  50694