Theorem preq1 4689

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 4589	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4118	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4582	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4582	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1559   ∪ cun 3900  {csn 4579  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-pr 4582

This theorem is referenced by:  preq2  4690  preq12  4691  preq1i  4692  preq1d  4695  tpeq1  4698  preq1b  4801  preq12b  4805  preq12bg  4808  prel12g  4819  elpreqpr  4822  opeq1  4828  prexOLD  5397  propeqop  5473  opthhausdorff  5483  opthhausdorff0  5484  fprg  7132  fnpr2g  7188  opthreg  9566  brdom7disj  10481  brdom6disj  10482  wunpr  10660  wunex2  10689  wuncval2  10698  grupr  10748  wwlktovf  14962  joindef  18396  meetdef  18410  pptbas  23055  usgredg4  29374  usgredg2vlem2  29383  usgredg2v  29384  nbgrval  29493  nb3grprlem2  29538  cusgredg  29581  cusgrfilem2  29613  usgredgsscusgredg  29616  rusgrnumwrdl2  29743  usgr2trlncl  29916  crctcshwlkn0lem6  29971  rusgrnumwwlks  30133  upgr3v3e3cycl  30338  upgr4cycl4dv4e  30343  eupth2lem3lem4  30389  nfrgr2v  30430  frgr3vlem1  30431  frgr3vlem2  30432  3vfriswmgr  30436  3cyclfrgrrn1  30443  4cycl2vnunb  30448  vdgn1frgrv2  30454  frgrncvvdeqlem8  30464  frgrncvvdeqlem9  30465  frgrwopregasn  30474  frgrwopreglem5ALT  30480  2clwwlk2clwwlklem  30504  cplgredgex  35431  altopthsn  36271  hdmap11lem2  42426  sge0prle  46935  meadjun  46996  elsprel  48041  prelspr  48052  sprsymrelfolem2  48059  reupr  48088  reuopreuprim  48092  clnbgrval  48404  cycl3grtri  48529  grimgrtri  48531  usgrgrtrirex  48532  isubgr3stgrlem4  48551  isubgr3stgrlem6  48553  isubgr3stgrlem7  48554  grlimprclnbgrvtx  48581  grlimgrtri  48585  usgrexmpl1tri  48607  gpg5nbgrvtx03star  48662  gpg5nbgr3star  48663  gpg3kgrtriex  48671  pgnbgreunbgrlem1  48695  pgnbgreunbgrlem2lem1  48696  pgnbgreunbgrlem2lem2  48697  pgnbgreunbgrlem2lem3  48698  pgnbgreunbgrlem4  48701  pgnbgreunbgrlem5lem1  48702  pgnbgreunbgrlem5lem2  48703  pgnbgreunbgrlem5lem3  48704  pgnbgreunbgr  48707  grlimedgnedg  48713  inlinecirc02plem  49368