Theorem 1st2nd2 7981

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4573   × cxp 5629  ‘cfv 6498  1^st c1st 7940  2^nd c2nd 7941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fv 6506  df-1st 7942  df-2nd 7943

This theorem is referenced by:  1st2ndb  7982  xpopth  7983  eqop  7984  2nd1st  7991  1st2nd  7992  opiota  8012  fimaproj  8085  disjen  9072  xpmapenlem  9082  mapunen  9084  djulf1o  9836  djurf1o  9837  djur  9843  r0weon  9934  enqbreq2  10843  nqereu  10852  lterpq  10893  elreal2  11055  cnref1o  12935  ruclem6  16202  ruclem8  16204  ruclem9  16205  ruclem12  16208  eucalgval  16551  eucalginv  16553  eucalglt  16554  eucalg  16556  qnumdenbi  16714  isstruct2  17119  xpsff1o  17531  comfffval2  17667  comfeq  17672  idfucl  17848  funcpropd  17869  coapm  18038  xpccatid  18154  1stfcl  18163  2ndfcl  18164  1st2ndprf  18172  xpcpropd  18174  evlfcl  18188  hofcl  18225  hofpropd  18233  yonedalem3  18246  gsum2dlem2  19946  mdetunilem9  22585  tx1cn  23574  tx2cn  23575  txdis  23597  txlly  23601  txnlly  23602  txhaus  23612  txkgen  23617  txconn  23654  utop3cls  24216  ucnima  24245  fmucndlem  24255  psmetxrge0  24278  imasdsf1olem  24338  cnheiborlem  24921  caublcls  25276  bcthlem1  25291  bcthlem2  25292  bcthlem4  25294  bcthlem5  25295  ovolfcl  25433  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovolfsval  25437  ovolicc2lem1  25484  ovolicc2lem5  25488  ovolfs2  25538  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2a  25549  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombllem6  25555  dyadmbl  25567  fsumvma  27176  opreu2reuALT  32546  ofpreima  32738  ofpreima2  32739  elrgspnsubrunlem2  33309  erler  33326  1stmbfm  34404  2ndmbfm  34405  sibfof  34484  oddpwdcv  34499  txsconnlem  35422  mpst123  35722  bj-elid4  37482  bj-elid6  37484  poimirlem4  37945  poimirlem26  37967  poimirlem27  37968  mblfinlem1  37978  mblfinlem2  37979  ftc2nc  38023  heiborlem8  38139  dvhgrp  41553  dvhlveclem  41554  fvovco  45623  dvnprodlem1  46374  volioof  46415  fvvolioof  46417  fvvolicof  46419  etransclem44  46706  ovolval3  47075  ovolval4lem1  47077  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  smfpimbor1lem1  47226  rrx2xpref1o  49194  2oppf  49607  eloppf  49608  funcoppc5  49620  swapf2f1oa  49752  swapfida  49755  swapffunca  49759  swapfiso  49760  cofuswapf1  49769  cofuswapf2  49770  fuco2eld2  49789  fuco11b  49812  fuco11bALT  49813  fucoco2  49833  fucofunca  49835  fucolid  49836  fucorid  49837  precofvalALT  49843  reldmlan2  50092  reldmran2  50093  rellan  50098  relran  50099  ranval3  50106  ranrcl4lem  50113  ranup  50117