Theorem preq1 4671

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3936  {csn 4569  {cpr 4571

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-sn 4570  df-pr 4572

This theorem is referenced by:  preq2  4672  preq12  4673  preq1i  4674  preq1d  4677  tpeq1  4680  preq1b  4779  preq12b  4783  preq12bg  4786  prel12g  4796  elpreqpr  4799  elpr2elpr  4801  opeq1  4805  uniprg  4858  intprg  4912  prex  5335  propeqop  5399  opthhausdorff  5409  opthhausdorff0  5410  fprg  6919  fnpr2g  6975  opthreg  9083  brdom7disj  9955  brdom6disj  9956  wunpr  10133  wunex2  10162  wuncval2  10171  grupr  10221  wwlktovf  14322  joindef  17616  meetdef  17630  pptbas  21618  usgredg4  27001  usgredg2vlem2  27010  usgredg2v  27011  nbgrval  27120  nb3grprlem2  27165  cusgredg  27208  cusgrfilem2  27240  usgredgsscusgredg  27243  rusgrnumwrdl2  27370  usgr2trlncl  27543  crctcshwlkn0lem6  27595  rusgrnumwwlks  27755  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  eupth2lem3lem4  28012  nfrgr2v  28053  frgr3vlem1  28054  frgr3vlem2  28055  3vfriswmgr  28059  3cyclfrgrrn1  28066  4cycl2vnunb  28071  vdgn1frgrv2  28077  frgrncvvdeqlem8  28087  frgrncvvdeqlem9  28088  frgrwopregasn  28097  frgrwopreglem5ALT  28103  2clwwlk2clwwlklem  28127  cplgredgex  32369  altopthsn  33424  hdmap11lem2  38980  sge0prle  42690  meadjun  42751  elsprel  43644  prelspr  43655  sprsymrelfolem2  43662  reupr  43691  reuopreuprim  43695  isomuspgrlem2d  44003  inlinecirc02plem  44780