Theorem preq1 4709

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 4611	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4142	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4604	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4604	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3924  {csn 4601  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  preq2  4710  preq12  4711  preq1i  4712  preq1d  4715  tpeq1  4718  preq1b  4822  preq12b  4826  preq12bg  4829  prel12g  4840  elpreqpr  4843  opeq1  4849  prex  5407  propeqop  5482  opthhausdorff  5492  opthhausdorff0  5493  fprg  7144  fnpr2g  7201  opthreg  9630  brdom7disj  10543  brdom6disj  10544  wunpr  10721  wunex2  10750  wuncval2  10759  grupr  10809  wwlktovf  14973  joindef  18384  meetdef  18398  pptbas  22944  usgredg4  29142  usgredg2vlem2  29151  usgredg2v  29152  nbgrval  29261  nb3grprlem2  29306  cusgredg  29349  cusgrfilem2  29382  usgredgsscusgredg  29385  rusgrnumwrdl2  29512  usgr2trlncl  29688  crctcshwlkn0lem6  29743  rusgrnumwwlks  29902  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  eupth2lem3lem4  30158  nfrgr2v  30199  frgr3vlem1  30200  frgr3vlem2  30201  3vfriswmgr  30205  3cyclfrgrrn1  30212  4cycl2vnunb  30217  vdgn1frgrv2  30223  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  frgrwopregasn  30243  frgrwopreglem5ALT  30249  2clwwlk2clwwlklem  30273  cplgredgex  35089  altopthsn  35925  hdmap11lem2  41807  sge0prle  46378  meadjun  46439  elsprel  47437  prelspr  47448  sprsymrelfolem2  47455  reupr  47484  reuopreuprim  47488  clnbgrval  47784  cycl3grtri  47907  grimgrtri  47909  usgrgrtrirex  47910  isubgr3stgrlem4  47929  isubgr3stgrlem6  47931  isubgr3stgrlem7  47932  grlimgrtri  47956  usgrexmpl1tri  47977  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  gpg3kgrtriex  48039  inlinecirc02plem  48714