Theorem 1st2nd2 8053

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4632   × cxp 5683  ‘cfv 6561  1^st c1st 8012  2^nd c2nd 8013

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-2nd 8015

This theorem is referenced by:  1st2ndb  8054  xpopth  8055  eqop  8056  2nd1st  8063  1st2nd  8064  opiota  8084  fimaproj  8160  disjen  9174  xpmapenlem  9184  mapunen  9186  djulf1o  9952  djurf1o  9953  djur  9959  r0weon  10052  enqbreq2  10960  nqereu  10969  lterpq  11010  elreal2  11172  cnref1o  13027  ruclem6  16271  ruclem8  16273  ruclem9  16274  ruclem12  16277  eucalgval  16619  eucalginv  16621  eucalglt  16622  eucalg  16624  qnumdenbi  16781  isstruct2  17186  xpsff1o  17612  comfffval2  17744  comfeq  17749  idfucl  17926  funcpropd  17947  coapm  18116  xpccatid  18233  1stfcl  18242  2ndfcl  18243  1st2ndprf  18251  xpcpropd  18253  evlfcl  18267  hofcl  18304  hofpropd  18312  yonedalem3  18325  gsum2dlem2  19989  mdetunilem9  22626  tx1cn  23617  tx2cn  23618  txdis  23640  txlly  23644  txnlly  23645  txhaus  23655  txkgen  23660  txconn  23697  utop3cls  24260  ucnima  24290  fmucndlem  24300  psmetxrge0  24323  imasdsf1olem  24383  cnheiborlem  24986  caublcls  25343  bcthlem1  25358  bcthlem2  25359  bcthlem4  25361  bcthlem5  25362  ovolfcl  25501  ovolfioo  25502  ovolficc  25503  ovolficcss  25504  ovolfsval  25505  ovolicc2lem1  25552  ovolicc2lem5  25556  ovolfs2  25606  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2a  25617  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombllem6  25623  dyadmbl  25635  fsumvma  27257  opreu2reuALT  32496  ofpreima  32675  ofpreima2  32676  elrgspnsubrunlem2  33252  erler  33269  1stmbfm  34262  2ndmbfm  34263  sibfof  34342  oddpwdcv  34357  txsconnlem  35245  mpst123  35545  bj-elid4  37169  bj-elid6  37171  poimirlem4  37631  poimirlem26  37653  poimirlem27  37654  mblfinlem1  37664  mblfinlem2  37665  ftc2nc  37709  heiborlem8  37825  dvhgrp  41109  dvhlveclem  41110  fvovco  45198  dvnprodlem1  45961  volioof  46002  fvvolioof  46004  fvvolicof  46006  etransclem44  46293  ovolval3  46662  ovolval4lem1  46664  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  smfpimbor1lem1  46813  rrx2xpref1o  48639  swapf2f1oa  48983  swapfida  48986  swapffunca  48990  swapfiso  48991  cofuswapf1  48994  cofuswapf2  48995  fuco2eld2  49009  fuco11b  49032  fuco11bALT  49033  fucoco2  49053  fucofunca  49055  fucolid  49056  fucorid  49057  precofvalALT  49063