Theorem preq12 4214

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  preq12i  4217  preq12d  4220  ssprsseq  4297  preq12b  4322  prnebg  4329  snex  4835  relop  5194  opthreg  8398  wwlktovfo  13549  joinval  16828  meetval  16842  ipole  16981  sylow1  17841  frgpuplem  18008  sizeusglecusglem1  26012  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  usg2wlkeq  26236  usg2wlkonot  26410  imarnf1pr  40326  uspgr2wlkeq  40854  1wlkres  40879  1wlkp1lem8  40889  usgr2pthlem  40969  21wlkdlem10  41142  11wlkdlem4  41307  31wlkdlem6  41332  31wlkdlem10  41336