Theorem xpsng 7011

Description: The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)

Assertion

Ref	Expression
xpsng	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩})

Proof of Theorem xpsng

Step	Hyp	Ref	Expression
1		fconstg 6661	. . 3 ⊢ (𝐵 ∈ 𝑊 → ({𝐴} × {𝐵}):{𝐴}⟶{𝐵})
2	1	adantl 482	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}):{𝐴}⟶{𝐵})
3		fsng 7009	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (({𝐴} × {𝐵}):{𝐴}⟶{𝐵} ↔ ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩}))
4	2, 3	mpbid 231	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩})

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {csn 4561  ⟨cop 4567   × cxp 5587  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440

This theorem is referenced by:  xpprsng  7012  xpsn  7013  f1o2sn  7014  residpr  7015  fmptsn  7039  f1ofvswap  7178  mposn  7943  repsw1  14496  s1co  14546  intopsn  18338  grp1inv  18683  psgnsn  19128  ixpsnbasval  20480  mat1dimelbas  21620  mat1dimscm  21624  mat1dimmul  21625  mat1f1o  21627  m1detdiag  21746  pt1hmeo  22957  cosnop  31028  cshw1s2  31232  nosupbnd2lem1  33918  rngosn3  36082  fmptsnxp  42705  lmod1zr  45834