Theorem 1st2nd2 8040

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ⟨cop 4834   × cxp 5648  ‘cfv 6538  1^st c1st 7999  2^nd c2nd 8000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001  df-2nd 8002

This theorem is used by:  1st2ndb  8041  xpopth  8042  eqop  8043  2nd1st  8049  1st2nd  8050  opiota  8070  fimaproj  8154  disjen  9156  xpmapenlem  9166  mapunen  9168  djulf1o  9996  djurf1o  9997  djur  10003  r0weon  10094  enqbreq2  11008  nqereu  11017  lterpq  11058  elreal2  11220  cnref1o  13116  ruclem6  16408  ruclem8  16410  ruclem9  16411  ruclem12  16414  eucalgval  16762  eucalginv  16764  eucalglt  16765  eucalg  16767  qnumdenbi  16925  isstruct2  17332  xpsff1o  17744  comfffval2  17880  comfeq  17885  idfucl  18061  funcpropd  18082  coapm  18251  xpccatid  18367  1stfcl  18376  2ndfcl  18377  1st2ndprf  18385  xpcpropd  18387  evlfcl  18401  hofcl  18438  hofpropd  18446  yonedalem3  18459  gsum2dlem2  20190  mdetunilem9  22940  tx1cn  23933  tx2cn  23934  txdis  23956  txlly  23960  txnlly  23961  txhaus  23971  txkgen  23976  txconn  24013  utop3cls  24575  ucnima  24604  fmucndlem  24614  psmetxrge0  24637  imasdsf1olem  24697  cnheiborlem  25280  caublcls  25635  bcthlem1  25650  bcthlem2  25651  bcthlem4  25653  bcthlem5  25654  ovolfcl  25792  ovolfioo  25793  ovolficc  25794  ovolficcss  25795  ovolfsval  25796  ovolicc2lem1  25843  ovolicc2lem5  25847  ovolfs2  25897  uniiccdif  25904  uniioovol  25905  uniiccvol  25906  uniioombllem2a  25908  uniioombllem2  25909  uniioombllem3a  25910  uniioombllem3  25911  uniioombllem4  25912  uniioombllem5  25913  uniioombllem6  25914  dyadmbl  25926  fsumvma  27545  opreu2reuALT  33120  ofpreima  33306  ofpreima2  33307  elrgspnsubrunlem2  33855  erler  33872  1stmbfm  34938  2ndmbfm  34939  sibfof  35018  oddpwdcv  35033  txsconnlem  36091  mpst123  36391  bj-elid4  38182  bj-elid6  38184  poimirlem4  38635  poimirlem26  38657  poimirlem27  38658  mblfinlem1  38668  mblfinlem2  38669  ftc2nc  38713  heiborlem8  38845  dvhgrp  42257  dvhlveclem  42258  fvovco  46301  dvnprodlem1  47049  volioof  47090  fvvolioof  47092  fvvolicof  47094  etransclem44  47381  ovolval3  47750  ovolval4lem1  47752  ovolval5lem2  47756  ovnovollem1  47759  ovnovollem2  47760  smfpimbor1lem1  47901  2oppf  50341  eloppf  50342  funcoppc5  50354  swapf2f1oa  50492  swapfida  50495  swapffunca  50499  swapfiso  50500  cofuswapf1  50509  cofuswapf2  50510  fuco2eld2  50529  fuco11b  50552  fuco11bALT  50553  fucoco2  50573  fucofunca  50575  fucolid  50576  fucorid  50577  precofvalALT  50596  reldmlan2  50893  reldmran2  50894  rellan  50899  relran  50900  ranval3  50907  ranrcl4lem  50914  ranup  50918