Theorem preq12 4688

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 4686	. 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2		preq2 4687	. 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
3	1, 2	sylan9eq 2786	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  preq12i  4691  preq12d  4694  ssprsseq  4777  preq12b  4802  prnebg  4808  preq12nebg  4815  opthprneg  4817  elpr2elpr  4821  relop  5790  opthreg  9508  hashle2pr  14384  wwlktovfo  14865  joinval  18281  meetval  18295  ipole  18440  sylow1  19516  frgpuplem  19685  uspgr2wlkeq  29625  wlkres  29648  wlkp1lem8  29658  usgr2pthlem  29742  2wlkdlem10  29914  1wlkdlem4  30118  3wlkdlem6  30143  3wlkdlem10  30147  pfxwlk  35166  oppr  47067  imarnf1pr  47319  elsprel  47512  sprsymrelf1lem  47528  sprsymrelf  47532  paireqne  47548  sbcpr  47558  isuspgrimlem  47932  grtrif1o  47979