Theorem preq1 4736

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 4637	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4161	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4630	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4630	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3945  {csn 4627  {cpr 4629

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  preq2  4737  preq12  4738  preq1i  4739  preq1d  4742  tpeq1  4745  preq1b  4846  preq12b  4850  preq12bg  4853  prel12g  4863  elpreqpr  4866  elpr2elpr  4868  opeq1  4872  uniprgOLD  4927  intprgOLD  4987  prex  5431  propeqop  5506  opthhausdorff  5516  opthhausdorff0  5517  fprg  7149  fnpr2g  7208  opthreg  9609  brdom7disj  10522  brdom6disj  10523  wunpr  10700  wunex2  10729  wuncval2  10738  grupr  10788  wwlktovf  14903  joindef  18325  meetdef  18339  pptbas  22502  usgredg4  28463  usgredg2vlem2  28472  usgredg2v  28473  nbgrval  28582  nb3grprlem2  28627  cusgredg  28670  cusgrfilem2  28702  usgredgsscusgredg  28705  rusgrnumwrdl2  28832  usgr2trlncl  29006  crctcshwlkn0lem6  29058  rusgrnumwwlks  29217  upgr3v3e3cycl  29422  upgr4cycl4dv4e  29427  eupth2lem3lem4  29473  nfrgr2v  29514  frgr3vlem1  29515  frgr3vlem2  29516  3vfriswmgr  29520  3cyclfrgrrn1  29527  4cycl2vnunb  29532  vdgn1frgrv2  29538  frgrncvvdeqlem8  29548  frgrncvvdeqlem9  29549  frgrwopregasn  29558  frgrwopreglem5ALT  29564  2clwwlk2clwwlklem  29588  cplgredgex  34099  altopthsn  34921  hdmap11lem2  40701  sge0prle  45103  meadjun  45164  elsprel  46129  prelspr  46140  sprsymrelfolem2  46147  reupr  46176  reuopreuprim  46180  isomuspgrlem2d  46485  inlinecirc02plem  47425