Theorem preq1 4687

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 4589	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4120	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4582	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4582	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3903  {csn 4579  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  preq2  4688  preq12  4689  preq1i  4690  preq1d  4693  tpeq1  4696  preq1b  4800  preq12b  4804  preq12bg  4807  prel12g  4818  elpreqpr  4821  opeq1  4827  prex  5379  propeqop  5454  opthhausdorff  5464  opthhausdorff0  5465  fprg  7093  fnpr2g  7150  opthreg  9533  brdom7disj  10444  brdom6disj  10445  wunpr  10622  wunex2  10651  wuncval2  10660  grupr  10710  wwlktovf  14881  joindef  18298  meetdef  18312  pptbas  22911  usgredg4  29180  usgredg2vlem2  29189  usgredg2v  29190  nbgrval  29299  nb3grprlem2  29344  cusgredg  29387  cusgrfilem2  29420  usgredgsscusgredg  29423  rusgrnumwrdl2  29550  usgr2trlncl  29723  crctcshwlkn0lem6  29778  rusgrnumwwlks  29937  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupth2lem3lem4  30193  nfrgr2v  30234  frgr3vlem1  30235  frgr3vlem2  30236  3vfriswmgr  30240  3cyclfrgrrn1  30247  4cycl2vnunb  30252  vdgn1frgrv2  30258  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  frgrwopregasn  30278  frgrwopreglem5ALT  30284  2clwwlk2clwwlklem  30308  cplgredgex  35096  altopthsn  35937  hdmap11lem2  41824  sge0prle  46386  meadjun  46447  elsprel  47463  prelspr  47474  sprsymrelfolem2  47481  reupr  47510  reuopreuprim  47514  clnbgrval  47810  cycl3grtri  47935  grimgrtri  47937  usgrgrtrirex  47938  isubgr3stgrlem4  47957  isubgr3stgrlem6  47959  isubgr3stgrlem7  47960  grlimprclnbgrvtx  47987  grlimgrtri  47991  usgrexmpl1tri  48013  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  gpg3kgrtriex  48077  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5lem1  48108  pgnbgreunbgrlem5lem2  48109  pgnbgreunbgrlem5lem3  48110  pgnbgreunbgr  48113  grlimedgnedg  48119  inlinecirc02plem  48775