Theorem preq1 4695

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 4595	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4123	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4588	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4588	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1563   ∪ cun 3905  {csn 4585  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  preq2  4696  preq12  4697  preq1i  4698  preq1d  4701  tpeq1  4704  preq1b  4806  preq12b  4810  preq12bg  4813  prel12g  4824  elpreqpr  4827  opeq1  4833  prexOLD  5404  propeqop  5480  opthhausdorff  5490  opthhausdorff0  5491  fprg  7142  fnpr2g  7198  opthreg  9575  brdom7disj  10503  brdom6disj  10504  wunpr  10682  wunex2  10711  wuncval2  10720  grupr  10770  wwlktovf  14981  joindef  18418  meetdef  18432  pptbas  23122  usgredg4  29472  usgredg2vlem2  29481  usgredg2v  29482  nbgrval  29591  nb3grprlem2  29636  cusgredg  29679  cusgrfilem2  29711  usgredgsscusgredg  29714  rusgrnumwrdl2  29841  usgr2trlncl  30014  crctcshwlkn0lem6  30069  rusgrnumwwlks  30231  upgr3v3e3cycl  30436  upgr4cycl4dv4e  30441  eupth2lem3lem4  30487  nfrgr2v  30528  frgr3vlem1  30529  frgr3vlem2  30530  3vfriswmgr  30534  3cyclfrgrrn1  30541  4cycl2vnunb  30546  vdgn1frgrv2  30552  frgrncvvdeqlem8  30562  frgrncvvdeqlem9  30563  frgrwopregasn  30572  frgrwopreglem5ALT  30578  2clwwlk2clwwlklem  30602  cplgredgex  35479  altopthsn  36319  hdmap11lem2  42473  sge0prle  46974  meadjun  47035  elsprel  48080  prelspr  48091  sprsymrelfolem2  48098  reupr  48127  reuopreuprim  48131  clnbgrval  48443  cycl3grtri  48568  grimgrtri  48570  usgrgrtrirex  48571  isubgr3stgrlem4  48590  isubgr3stgrlem6  48592  isubgr3stgrlem7  48593  grlimprclnbgrvtx  48620  grlimgrtri  48624  usgrexmpl1tri  48646  gpg5nbgrvtx03star  48701  gpg5nbgr3star  48702  gpg3kgrtriex  48710  pgnbgreunbgrlem1  48734  pgnbgreunbgrlem2lem1  48735  pgnbgreunbgrlem2lem2  48736  pgnbgreunbgrlem2lem3  48737  pgnbgreunbgrlem4  48740  pgnbgreunbgrlem5lem1  48741  pgnbgreunbgrlem5lem2  48742  pgnbgreunbgrlem5lem3  48743  pgnbgreunbgr  48746  grlimedgnedg  48752  inlinecirc02plem  49418