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 2824	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4592  df-pr 4594

This theorem is referenced by:  preq12i  4706  preq12d  4709  ssprsseq  4792  preq12b  4816  prnebg  4822  preq12nebg  4829  opthprneg  4831  elpr2elpr  4835  relop  5834  opthreg  9583  hashle2pr  14510  wwlktovfo  14991  joinval  18427  meetval  18441  ipole  18586  sylow1  19669  frgpuplem  19838  uspgr2wlkeq  29932  wlkres  29955  wlkp1lem8  29965  usgr2pthlem  30049  2wlkdlem10  30221  1wlkdlem4  30428  3wlkdlem6  30453  3wlkdlem10  30457  pfxwlk  35511  oppr  47649  imarnf1pr  47901  elsprel  48106  sprsymrelf1lem  48122  sprsymrelf  48126  paireqne  48142  sbcpr  48152  isuspgrimlem  48542  grtrif1o  48589