Theorem preq1 4629

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 4535	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4069	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4528	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4528	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2818	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3858  {csn 4525  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-sn 4526  df-pr 4528

This theorem is referenced by:  preq2  4630  preq12  4631  preq1i  4632  preq1d  4635  tpeq1  4638  preq1b  4737  preq12b  4741  preq12bg  4744  prel12g  4754  elpreqpr  4757  elpr2elpr  4759  opeq1  4764  opeq1OLD  4765  uniprgOLD  4821  intprgOLD  4877  prex  5304  propeqop  5369  opthhausdorff  5379  opthhausdorff0  5380  fprg  6913  fnpr2g  6969  opthreg  9119  brdom7disj  9996  brdom6disj  9997  wunpr  10174  wunex2  10203  wuncval2  10212  grupr  10262  wwlktovf  14372  joindef  17685  meetdef  17699  pptbas  21713  usgredg4  27111  usgredg2vlem2  27120  usgredg2v  27121  nbgrval  27230  nb3grprlem2  27275  cusgredg  27318  cusgrfilem2  27350  usgredgsscusgredg  27353  rusgrnumwrdl2  27480  usgr2trlncl  27653  crctcshwlkn0lem6  27705  rusgrnumwwlks  27864  upgr3v3e3cycl  28069  upgr4cycl4dv4e  28074  eupth2lem3lem4  28120  nfrgr2v  28161  frgr3vlem1  28162  frgr3vlem2  28163  3vfriswmgr  28167  3cyclfrgrrn1  28174  4cycl2vnunb  28179  vdgn1frgrv2  28185  frgrncvvdeqlem8  28195  frgrncvvdeqlem9  28196  frgrwopregasn  28205  frgrwopreglem5ALT  28211  2clwwlk2clwwlklem  28235  cplgredgex  32602  altopthsn  33838  hdmap11lem2  39444  sge0prle  43434  meadjun  43495  elsprel  44388  prelspr  44399  sprsymrelfolem2  44406  reupr  44435  reuopreuprim  44439  isomuspgrlem2d  44744  inlinecirc02plem  45593