Theorem preq1 4677

Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)

Assertion

Ref	Expression
preq1	⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Proof of Theorem preq1

Step	Hyp	Ref	Expression
1		sneq 4577	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4107	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4570	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4570	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3887  {csn 4567  {cpr 4569

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  preq2  4678  preq12  4679  preq1i  4680  preq1d  4683  tpeq1  4686  preq1b  4789  preq12b  4793  preq12bg  4796  prel12g  4807  elpreqpr  4810  opeq1  4816  prexOLD  5385  propeqop  5461  opthhausdorff  5471  opthhausdorff0  5472  fprg  7109  fnpr2g  7165  opthreg  9539  brdom7disj  10453  brdom6disj  10454  wunpr  10632  wunex2  10661  wuncval2  10670  grupr  10720  wwlktovf  14918  joindef  18340  meetdef  18354  pptbas  22973  usgredg4  29286  usgredg2vlem2  29295  usgredg2v  29296  nbgrval  29405  nb3grprlem2  29450  cusgredg  29493  cusgrfilem2  29525  usgredgsscusgredg  29528  rusgrnumwrdl2  29655  usgr2trlncl  29828  crctcshwlkn0lem6  29883  rusgrnumwwlks  30045  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth2lem3lem4  30301  nfrgr2v  30342  frgr3vlem1  30343  frgr3vlem2  30344  3vfriswmgr  30348  3cyclfrgrrn1  30355  4cycl2vnunb  30360  vdgn1frgrv2  30366  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  frgrwopregasn  30386  frgrwopreglem5ALT  30392  2clwwlk2clwwlklem  30416  cplgredgex  35303  altopthsn  36143  hdmap11lem2  42288  sge0prle  46829  meadjun  46890  elsprel  47935  prelspr  47946  sprsymrelfolem2  47953  reupr  47982  reuopreuprim  47986  clnbgrval  48298  cycl3grtri  48423  grimgrtri  48425  usgrgrtrirex  48426  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  grlimprclnbgrvtx  48475  grlimgrtri  48479  usgrexmpl1tri  48501  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpg3kgrtriex  48565  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgr  48601  grlimedgnedg  48607  inlinecirc02plem  49262