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 1540   ∈ wcel 2109  ⟨cop 4595   × cxp 5636  ‘cfv 6511  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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-1st 7968  df-2nd 7969

This theorem is referenced by:  1st2ndb  8008  xpopth  8009  eqop  8010  2nd1st  8017  1st2nd  8018  opiota  8038  fimaproj  8114  disjen  9098  xpmapenlem  9108  mapunen  9110  djulf1o  9865  djurf1o  9866  djur  9872  r0weon  9965  enqbreq2  10873  nqereu  10882  lterpq  10923  elreal2  11085  cnref1o  12944  ruclem6  16203  ruclem8  16205  ruclem9  16206  ruclem12  16209  eucalgval  16552  eucalginv  16554  eucalglt  16555  eucalg  16557  qnumdenbi  16714  isstruct2  17119  xpsff1o  17530  comfffval2  17662  comfeq  17667  idfucl  17843  funcpropd  17864  coapm  18033  xpccatid  18149  1stfcl  18158  2ndfcl  18159  1st2ndprf  18167  xpcpropd  18169  evlfcl  18183  hofcl  18220  hofpropd  18228  yonedalem3  18241  gsum2dlem2  19901  mdetunilem9  22507  tx1cn  23496  tx2cn  23497  txdis  23519  txlly  23523  txnlly  23524  txhaus  23534  txkgen  23539  txconn  23576  utop3cls  24139  ucnima  24168  fmucndlem  24178  psmetxrge0  24201  imasdsf1olem  24261  cnheiborlem  24853  caublcls  25209  bcthlem1  25224  bcthlem2  25225  bcthlem4  25227  bcthlem5  25228  ovolfcl  25367  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovolfsval  25371  ovolicc2lem1  25418  ovolicc2lem5  25422  ovolfs2  25472  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2a  25483  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  dyadmbl  25501  fsumvma  27124  opreu2reuALT  32406  ofpreima  32589  ofpreima2  32590  elrgspnsubrunlem2  33199  erler  33216  1stmbfm  34251  2ndmbfm  34252  sibfof  34331  oddpwdcv  34346  txsconnlem  35227  mpst123  35527  bj-elid4  37156  bj-elid6  37158  poimirlem4  37618  poimirlem26  37640  poimirlem27  37641  mblfinlem1  37651  mblfinlem2  37652  ftc2nc  37696  heiborlem8  37812  dvhgrp  41101  dvhlveclem  41102  fvovco  45187  dvnprodlem1  45944  volioof  45985  fvvolioof  45987  fvvolicof  45989  etransclem44  46276  ovolval3  46645  ovolval4lem1  46647  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  smfpimbor1lem1  46796  rrx2xpref1o  48707  2oppf  49121  eloppf  49122  funcoppc5  49134  swapf2f1oa  49266  swapfida  49269  swapffunca  49273  swapfiso  49274  cofuswapf1  49283  cofuswapf2  49284  fuco2eld2  49303  fuco11b  49326  fuco11bALT  49327  fucoco2  49347  fucofunca  49349  fucolid  49350  fucorid  49351  precofvalALT  49357  reldmlan2  49606  reldmran2  49607  rellan  49612  relran  49613  ranval3  49620  ranrcl4lem  49627  ranup  49631