Theorem preq1 4686

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3900  {csn 4576  {cpr 4578

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  preq2  4687  preq12  4688  preq1i  4689  preq1d  4692  tpeq1  4695  preq1b  4798  preq12b  4802  preq12bg  4805  prel12g  4816  elpreqpr  4819  opeq1  4825  prex  5375  propeqop  5447  opthhausdorff  5457  opthhausdorff0  5458  fprg  7088  fnpr2g  7144  opthreg  9508  brdom7disj  10422  brdom6disj  10423  wunpr  10600  wunex2  10629  wuncval2  10638  grupr  10688  wwlktovf  14863  joindef  18280  meetdef  18294  pptbas  22924  usgredg4  29196  usgredg2vlem2  29205  usgredg2v  29206  nbgrval  29315  nb3grprlem2  29360  cusgredg  29403  cusgrfilem2  29436  usgredgsscusgredg  29439  rusgrnumwrdl2  29566  usgr2trlncl  29739  crctcshwlkn0lem6  29794  rusgrnumwwlks  29953  upgr3v3e3cycl  30158  upgr4cycl4dv4e  30163  eupth2lem3lem4  30209  nfrgr2v  30250  frgr3vlem1  30251  frgr3vlem2  30252  3vfriswmgr  30256  3cyclfrgrrn1  30263  4cycl2vnunb  30268  vdgn1frgrv2  30274  frgrncvvdeqlem8  30284  frgrncvvdeqlem9  30285  frgrwopregasn  30294  frgrwopreglem5ALT  30300  2clwwlk2clwwlklem  30324  cplgredgex  35163  altopthsn  36001  hdmap11lem2  41887  sge0prle  46445  meadjun  46506  elsprel  47512  prelspr  47523  sprsymrelfolem2  47530  reupr  47559  reuopreuprim  47563  clnbgrval  47859  cycl3grtri  47984  grimgrtri  47986  usgrgrtrirex  47987  isubgr3stgrlem4  48006  isubgr3stgrlem6  48008  isubgr3stgrlem7  48009  grlimprclnbgrvtx  48036  grlimgrtri  48040  usgrexmpl1tri  48062  gpg5nbgrvtx03star  48117  gpg5nbgr3star  48118  gpg3kgrtriex  48126  pgnbgreunbgrlem1  48150  pgnbgreunbgrlem2lem1  48151  pgnbgreunbgrlem2lem2  48152  pgnbgreunbgrlem2lem3  48153  pgnbgreunbgrlem4  48156  pgnbgreunbgrlem5lem1  48157  pgnbgreunbgrlem5lem2  48158  pgnbgreunbgrlem5lem3  48159  pgnbgreunbgr  48162  grlimedgnedg  48168  inlinecirc02plem  48824