Theorem 1st2nd2 8007

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  ⟨cop 4626   × cxp 5664  ‘cfv 6533  1^st c1st 7966  2^nd c2nd 7967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6485  df-fun 6535  df-fv 6541  df-1st 7968  df-2nd 7969

This theorem is referenced by:  1st2ndb  8008  xpopth  8009  eqop  8010  2nd1st  8017  1st2nd  8018  opiota  8038  fimaproj  8115  disjen  9130  xpmapenlem  9140  mapunen  9142  djulf1o  9903  djurf1o  9904  djur  9910  r0weon  10003  enqbreq2  10911  nqereu  10920  lterpq  10961  elreal2  11123  cnref1o  12966  ruclem6  16175  ruclem8  16177  ruclem9  16178  ruclem12  16181  eucalgval  16516  eucalginv  16518  eucalglt  16519  eucalg  16521  qnumdenbi  16679  isstruct2  17081  xpsff1o  17512  comfffval2  17644  comfeq  17649  idfucl  17830  funcpropd  17852  coapm  18023  xpccatid  18142  1stfcl  18151  2ndfcl  18152  1st2ndprf  18160  xpcpropd  18163  evlfcl  18177  hofcl  18214  hofpropd  18222  yonedalem3  18235  gsum2dlem2  19881  mdetunilem9  22444  tx1cn  23435  tx2cn  23436  txdis  23458  txlly  23462  txnlly  23463  txhaus  23473  txkgen  23478  txconn  23515  utop3cls  24078  ucnima  24108  fmucndlem  24118  psmetxrge0  24141  imasdsf1olem  24201  cnheiborlem  24802  caublcls  25159  bcthlem1  25174  bcthlem2  25175  bcthlem4  25177  bcthlem5  25178  ovolfcl  25317  ovolfioo  25318  ovolficc  25319  ovolficcss  25320  ovolfsval  25321  ovolicc2lem1  25368  ovolicc2lem5  25372  ovolfs2  25422  uniiccdif  25429  uniioovol  25430  uniiccvol  25431  uniioombllem2a  25433  uniioombllem2  25434  uniioombllem3a  25435  uniioombllem3  25436  uniioombllem4  25437  uniioombllem5  25438  uniioombllem6  25439  dyadmbl  25451  fsumvma  27062  opreu2reuALT  32186  ofpreima  32359  ofpreima2  32360  1stmbfm  33748  2ndmbfm  33749  sibfof  33828  oddpwdcv  33843  txsconnlem  34720  mpst123  35020  bj-elid4  36539  bj-elid6  36541  poimirlem4  36982  poimirlem26  37004  poimirlem27  37005  mblfinlem1  37015  mblfinlem2  37016  ftc2nc  37060  heiborlem8  37176  dvhgrp  40468  dvhlveclem  40469  fvovco  44377  dvnprodlem1  45147  volioof  45188  fvvolioof  45190  fvvolicof  45192  etransclem44  45479  ovolval3  45848  ovolval4lem1  45850  ovolval5lem2  45854  ovnovollem1  45857  ovnovollem2  45858  smfpimbor1lem1  45999  rrx2xpref1o  47592