Theorem 1st2nd2 7970

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4585   × cxp 5621  ‘cfv 6486  1^st c1st 7929  2^nd c2nd 7930

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 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fv 6494  df-1st 7931  df-2nd 7932

This theorem is referenced by:  1st2ndb  7971  xpopth  7972  eqop  7973  2nd1st  7980  1st2nd  7981  opiota  8001  fimaproj  8075  disjen  9058  xpmapenlem  9068  mapunen  9070  djulf1o  9827  djurf1o  9828  djur  9834  r0weon  9925  enqbreq2  10833  nqereu  10842  lterpq  10883  elreal2  11045  cnref1o  12904  ruclem6  16162  ruclem8  16164  ruclem9  16165  ruclem12  16168  eucalgval  16511  eucalginv  16513  eucalglt  16514  eucalg  16516  qnumdenbi  16673  isstruct2  17078  xpsff1o  17489  comfffval2  17625  comfeq  17630  idfucl  17806  funcpropd  17827  coapm  17996  xpccatid  18112  1stfcl  18121  2ndfcl  18122  1st2ndprf  18130  xpcpropd  18132  evlfcl  18146  hofcl  18183  hofpropd  18191  yonedalem3  18204  gsum2dlem2  19868  mdetunilem9  22523  tx1cn  23512  tx2cn  23513  txdis  23535  txlly  23539  txnlly  23540  txhaus  23550  txkgen  23555  txconn  23592  utop3cls  24155  ucnima  24184  fmucndlem  24194  psmetxrge0  24217  imasdsf1olem  24277  cnheiborlem  24869  caublcls  25225  bcthlem1  25240  bcthlem2  25241  bcthlem4  25243  bcthlem5  25244  ovolfcl  25383  ovolfioo  25384  ovolficc  25385  ovolficcss  25386  ovolfsval  25387  ovolicc2lem1  25434  ovolicc2lem5  25438  ovolfs2  25488  uniiccdif  25495  uniioovol  25496  uniiccvol  25497  uniioombllem2a  25499  uniioombllem2  25500  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombllem6  25505  dyadmbl  25517  fsumvma  27140  opreu2reuALT  32439  ofpreima  32622  ofpreima2  32623  elrgspnsubrunlem2  33201  erler  33218  1stmbfm  34230  2ndmbfm  34231  sibfof  34310  oddpwdcv  34325  txsconnlem  35215  mpst123  35515  bj-elid4  37144  bj-elid6  37146  poimirlem4  37606  poimirlem26  37628  poimirlem27  37629  mblfinlem1  37639  mblfinlem2  37640  ftc2nc  37684  heiborlem8  37800  dvhgrp  41089  dvhlveclem  41090  fvovco  45174  dvnprodlem1  45931  volioof  45972  fvvolioof  45974  fvvolicof  45976  etransclem44  46263  ovolval3  46632  ovolval4lem1  46634  ovolval5lem2  46638  ovnovollem1  46641  ovnovollem2  46642  smfpimbor1lem1  46783  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