Theorem 1st2nd2 7972

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4586   × cxp 5622  ‘cfv 6492  1^st c1st 7931  2^nd c2nd 7932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  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 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7933  df-2nd 7934

This theorem is referenced by:  1st2ndb  7973  xpopth  7974  eqop  7975  2nd1st  7982  1st2nd  7983  opiota  8003  fimaproj  8077  disjen  9062  xpmapenlem  9072  mapunen  9074  djulf1o  9824  djurf1o  9825  djur  9831  r0weon  9922  enqbreq2  10831  nqereu  10840  lterpq  10881  elreal2  11043  cnref1o  12898  ruclem6  16160  ruclem8  16162  ruclem9  16163  ruclem12  16166  eucalgval  16509  eucalginv  16511  eucalglt  16512  eucalg  16514  qnumdenbi  16671  isstruct2  17076  xpsff1o  17488  comfffval2  17624  comfeq  17629  idfucl  17805  funcpropd  17826  coapm  17995  xpccatid  18111  1stfcl  18120  2ndfcl  18121  1st2ndprf  18129  xpcpropd  18131  evlfcl  18145  hofcl  18182  hofpropd  18190  yonedalem3  18203  gsum2dlem2  19900  mdetunilem9  22564  tx1cn  23553  tx2cn  23554  txdis  23576  txlly  23580  txnlly  23581  txhaus  23591  txkgen  23596  txconn  23633  utop3cls  24195  ucnima  24224  fmucndlem  24234  psmetxrge0  24257  imasdsf1olem  24317  cnheiborlem  24909  caublcls  25265  bcthlem1  25280  bcthlem2  25281  bcthlem4  25283  bcthlem5  25284  ovolfcl  25423  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovolfsval  25427  ovolicc2lem1  25474  ovolicc2lem5  25478  ovolfs2  25528  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2a  25539  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombllem6  25545  dyadmbl  25557  fsumvma  27180  opreu2reuALT  32551  ofpreima  32743  ofpreima2  32744  elrgspnsubrunlem2  33330  erler  33347  1stmbfm  34417  2ndmbfm  34418  sibfof  34497  oddpwdcv  34512  txsconnlem  35434  mpst123  35734  bj-elid4  37369  bj-elid6  37371  poimirlem4  37821  poimirlem26  37843  poimirlem27  37844  mblfinlem1  37854  mblfinlem2  37855  ftc2nc  37899  heiborlem8  38015  dvhgrp  41363  dvhlveclem  41364  fvovco  45433  dvnprodlem1  46186  volioof  46227  fvvolioof  46229  fvvolicof  46231  etransclem44  46518  ovolval3  46887  ovolval4lem1  46889  ovolval5lem2  46893  ovnovollem1  46896  ovnovollem2  46897  smfpimbor1lem1  47038  rrx2xpref1o  48960  2oppf  49373  eloppf  49374  funcoppc5  49386  swapf2f1oa  49518  swapfida  49521  swapffunca  49525  swapfiso  49526  cofuswapf1  49535  cofuswapf2  49536  fuco2eld2  49555  fuco11b  49578  fuco11bALT  49579  fucoco2  49599  fucofunca  49601  fucolid  49602  fucorid  49603  precofvalALT  49609  reldmlan2  49858  reldmran2  49859  rellan  49864  relran  49865  ranval3  49872  ranrcl4lem  49879  ranup  49883