Theorem preq1 4666

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 4568	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4092	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4561	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4561	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3881  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  preq2  4667  preq12  4668  preq1i  4669  preq1d  4672  tpeq1  4675  preq1b  4774  preq12b  4778  preq12bg  4781  prel12g  4791  elpreqpr  4794  elpr2elpr  4796  opeq1  4801  uniprgOLD  4856  intprgOLD  4912  prex  5350  propeqop  5415  opthhausdorff  5425  opthhausdorff0  5426  fprg  7009  fnpr2g  7068  opthreg  9306  brdom7disj  10218  brdom6disj  10219  wunpr  10396  wunex2  10425  wuncval2  10434  grupr  10484  wwlktovf  14599  joindef  18009  meetdef  18023  pptbas  22066  usgredg4  27487  usgredg2vlem2  27496  usgredg2v  27497  nbgrval  27606  nb3grprlem2  27651  cusgredg  27694  cusgrfilem2  27726  usgredgsscusgredg  27729  rusgrnumwrdl2  27856  usgr2trlncl  28029  crctcshwlkn0lem6  28081  rusgrnumwwlks  28240  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eupth2lem3lem4  28496  nfrgr2v  28537  frgr3vlem1  28538  frgr3vlem2  28539  3vfriswmgr  28543  3cyclfrgrrn1  28550  4cycl2vnunb  28555  vdgn1frgrv2  28561  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  frgrwopregasn  28581  frgrwopreglem5ALT  28587  2clwwlk2clwwlklem  28611  cplgredgex  32982  altopthsn  34190  hdmap11lem2  39783  sge0prle  43829  meadjun  43890  elsprel  44815  prelspr  44826  sprsymrelfolem2  44833  reupr  44862  reuopreuprim  44866  isomuspgrlem2d  45171  inlinecirc02plem  46020