Theorem preq12 4703

Description: Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Assertion

Ref	Expression
preq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Proof of Theorem preq12

Step	Hyp	Ref	Expression
1		preq1 4701	. 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2		preq2 4702	. 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
3	1, 2	sylan9eq 2820	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  preq12i  4706  preq12d  4709  ssprsseq  4793  preq12b  4817  prnebg  4823  preq12nebg  4830  opthprneg  4832  elpr2elpr  4836  relop  5838  opthreg  9590  hashle2pr  14527  wwlktovfo  15014  joinval  18448  meetval  18462  ipole  18607  sylow1  19696  frgpuplem  19865  uspgr2wlkeq  30024  wlkres  30047  wlkp1lem8  30057  usgr2pthlem  30141  2wlkdlem10  30313  1wlkdlem4  30520  3wlkdlem6  30545  3wlkdlem10  30549  pfxwlk  35629  oppr  47800  imarnf1pr  48052  elsprel  48257  sprsymrelf1lem  48273  sprsymrelf  48277  paireqne  48293  sbcpr  48303  isuspgrimlem  48693  grtrif1o  48740