Theorem preq1 4670

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3886  {csn 4562  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-pr 4565

This theorem is referenced by:  preq2  4671  preq12  4672  preq1i  4673  preq1d  4676  tpeq1  4679  preq1b  4778  preq12b  4782  preq12bg  4785  prel12g  4795  elpreqpr  4798  elpr2elpr  4800  opeq1  4805  uniprgOLD  4860  intprgOLD  4916  prex  5356  propeqop  5422  opthhausdorff  5432  opthhausdorff0  5433  fprg  7036  fnpr2g  7095  opthreg  9385  brdom7disj  10296  brdom6disj  10297  wunpr  10474  wunex2  10503  wuncval2  10512  grupr  10562  wwlktovf  14680  joindef  18103  meetdef  18117  pptbas  22167  usgredg4  27593  usgredg2vlem2  27602  usgredg2v  27603  nbgrval  27712  nb3grprlem2  27757  cusgredg  27800  cusgrfilem2  27832  usgredgsscusgredg  27835  rusgrnumwrdl2  27962  usgr2trlncl  28137  crctcshwlkn0lem6  28189  rusgrnumwwlks  28348  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  eupth2lem3lem4  28604  nfrgr2v  28645  frgr3vlem1  28646  frgr3vlem2  28647  3vfriswmgr  28651  3cyclfrgrrn1  28658  4cycl2vnunb  28663  vdgn1frgrv2  28669  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  frgrwopregasn  28689  frgrwopreglem5ALT  28695  2clwwlk2clwwlklem  28719  cplgredgex  33091  altopthsn  34272  hdmap11lem2  39863  sge0prle  43946  meadjun  44007  elsprel  44938  prelspr  44949  sprsymrelfolem2  44956  reupr  44985  reuopreuprim  44989  isomuspgrlem2d  45294  inlinecirc02plem  46143