Theorem preq1 4669

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 4577	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4138	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4570	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4570	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2881	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3934  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  preq2  4670  preq12  4671  preq1i  4672  preq1d  4675  tpeq1  4678  preq1b  4777  preq12b  4781  preq12bg  4784  prel12g  4794  elpreqpr  4797  elpr2elpr  4799  opeq1  4803  uniprg  4856  intprg  4910  prex  5333  propeqop  5397  opthhausdorff  5407  opthhausdorff0  5408  fprg  6917  fnpr2g  6973  opthreg  9081  brdom7disj  9953  brdom6disj  9954  wunpr  10131  wunex2  10160  wuncval2  10169  grupr  10219  wwlktovf  14320  joindef  17614  meetdef  17628  pptbas  21616  usgredg4  26999  usgredg2vlem2  27008  usgredg2v  27009  nbgrval  27118  nb3grprlem2  27163  cusgredg  27206  cusgrfilem2  27238  usgredgsscusgredg  27241  rusgrnumwrdl2  27368  usgr2trlncl  27541  crctcshwlkn0lem6  27593  rusgrnumwwlks  27753  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth2lem3lem4  28010  nfrgr2v  28051  frgr3vlem1  28052  frgr3vlem2  28053  3vfriswmgr  28057  3cyclfrgrrn1  28064  4cycl2vnunb  28069  vdgn1frgrv2  28075  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  frgrwopregasn  28095  frgrwopreglem5ALT  28101  2clwwlk2clwwlklem  28125  cplgredgex  32367  altopthsn  33422  hdmap11lem2  38993  sge0prle  42703  meadjun  42764  elsprel  43657  prelspr  43668  sprsymrelfolem2  43675  reupr  43704  reuopreuprim  43708  isomuspgrlem2d  44016  inlinecirc02plem  44793