Theorem preq12 4490

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656  {cpr 4401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-sn 4400  df-pr 4402

This theorem is referenced by:  preq12i  4493  preq12d  4496  ssprsseq  4576  preq12b  4599  prnebg  4606  preq12nebg  4615  opthprneg  4617  snex  5131  relop  5509  opthreg  8797  opthregOLD  8799  hashle2pr  13555  wwlktovfo  14087  joinval  17365  meetval  17379  ipole  17518  sylow1  18376  frgpuplem  18545  uspgr2wlkeq  26950  wlkres  26976  wlkresOLD  26978  wlkp1lem8  26988  usgr2pthlem  27072  2wlkdlem10  27271  1wlkdlem4  27512  3wlkdlem6  27537  3wlkdlem10  27541  imarnf1pr  42179  paireqne  42275  isomuspgrlem2b  42561  isomuspgrlem2d  42563  elsprel  42586  sprsymrelf1lem  42602  sprsymrelf  42606