Theorem preq1 4690

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 4590	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4119	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4583	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4583	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3899  {csn 4580  {cpr 4582

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  preq2  4691  preq12  4692  preq1i  4693  preq1d  4696  tpeq1  4699  preq1b  4802  preq12b  4806  preq12bg  4809  prel12g  4820  elpreqpr  4823  opeq1  4829  prex  5382  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  fprg  7100  fnpr2g  7156  opthreg  9527  brdom7disj  10441  brdom6disj  10442  wunpr  10620  wunex2  10649  wuncval2  10658  grupr  10708  wwlktovf  14879  joindef  18297  meetdef  18311  pptbas  22952  usgredg4  29290  usgredg2vlem2  29299  usgredg2v  29300  nbgrval  29409  nb3grprlem2  29454  cusgredg  29497  cusgrfilem2  29530  usgredgsscusgredg  29533  rusgrnumwrdl2  29660  usgr2trlncl  29833  crctcshwlkn0lem6  29888  rusgrnumwwlks  30050  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eupth2lem3lem4  30306  nfrgr2v  30347  frgr3vlem1  30348  frgr3vlem2  30349  3vfriswmgr  30353  3cyclfrgrrn1  30360  4cycl2vnunb  30365  vdgn1frgrv2  30371  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  frgrwopregasn  30391  frgrwopreglem5ALT  30397  2clwwlk2clwwlklem  30421  cplgredgex  35315  altopthsn  36155  hdmap11lem2  42102  sge0prle  46645  meadjun  46706  elsprel  47721  prelspr  47732  sprsymrelfolem2  47739  reupr  47768  reuopreuprim  47772  clnbgrval  48068  cycl3grtri  48193  grimgrtri  48195  usgrgrtrirex  48196  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  grlimprclnbgrvtx  48245  grlimgrtri  48249  usgrexmpl1tri  48271  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  gpg3kgrtriex  48335  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  pgnbgreunbgr  48371  grlimedgnedg  48377  inlinecirc02plem  49032