Theorem preq12 4628

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  {cpr 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-sn 4523  df-pr 4525

This theorem is referenced by:  preq12i  4631  preq12d  4634  ssprsseq  4715  preq12b  4738  prnebg  4743  preq12nebg  4750  opthprneg  4752  snex  5300  relop  5690  opthreg  9114  hashle2pr  13887  wwlktovfo  14369  joinval  17681  meetval  17695  ipole  17834  sylow1  18795  frgpuplem  18965  uspgr2wlkeq  27534  wlkres  27559  wlkp1lem8  27569  usgr2pthlem  27651  2wlkdlem10  27820  1wlkdlem4  28024  3wlkdlem6  28049  3wlkdlem10  28053  pfxwlk  32601  oppr  43988  imarnf1pr  44206  elsprel  44360  sprsymrelf1lem  44376  sprsymrelf  44380  paireqne  44396  sbcpr  44406  isomuspgrlem2b  44714  isomuspgrlem2d  44716