Theorem preq1 4758

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 4658	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4190	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4651	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4651	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974  {csn 4648  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  preq2  4759  preq12  4760  preq1i  4761  preq1d  4764  tpeq1  4767  preq1b  4871  preq12b  4875  preq12bg  4878  prel12g  4888  elpreqpr  4891  opeq1  4897  prex  5452  propeqop  5526  opthhausdorff  5536  opthhausdorff0  5537  fprg  7189  fnpr2g  7247  opthreg  9687  brdom7disj  10600  brdom6disj  10601  wunpr  10778  wunex2  10807  wuncval2  10816  grupr  10866  wwlktovf  15005  joindef  18446  meetdef  18460  pptbas  23036  usgredg4  29252  usgredg2vlem2  29261  usgredg2v  29262  nbgrval  29371  nb3grprlem2  29416  cusgredg  29459  cusgrfilem2  29492  usgredgsscusgredg  29495  rusgrnumwrdl2  29622  usgr2trlncl  29796  crctcshwlkn0lem6  29848  rusgrnumwwlks  30007  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2lem3lem4  30263  nfrgr2v  30304  frgr3vlem1  30305  frgr3vlem2  30306  3vfriswmgr  30310  3cyclfrgrrn1  30317  4cycl2vnunb  30322  vdgn1frgrv2  30328  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  frgrwopregasn  30348  frgrwopreglem5ALT  30354  2clwwlk2clwwlklem  30378  cplgredgex  35088  altopthsn  35925  hdmap11lem2  41799  sge0prle  46322  meadjun  46383  elsprel  47349  prelspr  47360  sprsymrelfolem2  47367  reupr  47396  reuopreuprim  47400  clnbgrval  47696  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  usgrexmpl1tri  47840  inlinecirc02plem  48520