Theorem preq1 4678

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 4578	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4108	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4571	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4571	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3888  {csn 4568  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  preq2  4679  preq12  4680  preq1i  4681  preq1d  4684  tpeq1  4687  preq1b  4790  preq12b  4794  preq12bg  4797  prel12g  4808  elpreqpr  4811  opeq1  4817  prexOLD  5380  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  fprg  7102  fnpr2g  7158  opthreg  9530  brdom7disj  10444  brdom6disj  10445  wunpr  10623  wunex2  10652  wuncval2  10661  grupr  10711  wwlktovf  14909  joindef  18331  meetdef  18345  pptbas  22983  usgredg4  29300  usgredg2vlem2  29309  usgredg2v  29310  nbgrval  29419  nb3grprlem2  29464  cusgredg  29507  cusgrfilem2  29540  usgredgsscusgredg  29543  rusgrnumwrdl2  29670  usgr2trlncl  29843  crctcshwlkn0lem6  29898  rusgrnumwwlks  30060  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eupth2lem3lem4  30316  nfrgr2v  30357  frgr3vlem1  30358  frgr3vlem2  30359  3vfriswmgr  30363  3cyclfrgrrn1  30370  4cycl2vnunb  30375  vdgn1frgrv2  30381  frgrncvvdeqlem8  30391  frgrncvvdeqlem9  30392  frgrwopregasn  30401  frgrwopreglem5ALT  30407  2clwwlk2clwwlklem  30431  cplgredgex  35319  altopthsn  36159  hdmap11lem2  42302  sge0prle  46847  meadjun  46908  elsprel  47947  prelspr  47958  sprsymrelfolem2  47965  reupr  47994  reuopreuprim  47998  clnbgrval  48310  cycl3grtri  48435  grimgrtri  48437  usgrgrtrirex  48438  isubgr3stgrlem4  48457  isubgr3stgrlem6  48459  isubgr3stgrlem7  48460  grlimprclnbgrvtx  48487  grlimgrtri  48491  usgrexmpl1tri  48513  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  gpg3kgrtriex  48577  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  pgnbgreunbgr  48613  grlimedgnedg  48619  inlinecirc02plem  49274