Theorem preq1 4700

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 4600	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4122	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4593	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4593	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1570   ∪ cun 3904  {csn 4590  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  preq2  4701  preq12  4702  preq1i  4703  preq1d  4706  tpeq1  4709  preq1b  4812  preq12b  4816  preq12bg  4819  prel12g  4830  elpreqpr  4833  opeq1  4839  prexOLD  5416  propeqop  5492  opthhausdorff  5502  opthhausdorff0  5503  fprg  7154  fnpr2g  7210  opthreg  9588  brdom7disj  10516  brdom6disj  10517  wunpr  10695  wunex2  10724  wuncval2  10733  grupr  10783  wwlktovf  14995  joindef  18431  meetdef  18445  pptbas  23146  usgredg4  29548  usgredg2vlem2  29557  usgredg2v  29558  nbgrval  29667  nb3grprlem2  29712  cusgredg  29755  cusgrfilem2  29787  usgredgsscusgredg  29790  rusgrnumwrdl2  29917  usgr2trlncl  30090  crctcshwlkn0lem6  30145  rusgrnumwwlks  30307  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  eupth2lem3lem4  30563  nfrgr2v  30604  frgr3vlem1  30605  frgr3vlem2  30606  3vfriswmgr  30610  3cyclfrgrrn1  30617  4cycl2vnunb  30622  vdgn1frgrv2  30628  frgrncvvdeqlem8  30638  frgrncvvdeqlem9  30639  frgrwopregasn  30648  frgrwopreglem5ALT  30654  2clwwlk2clwwlklem  30678  cplgredgex  35594  altopthsn  36434  hdmap11lem2  42597  sge0prle  47098  meadjun  47159  elsprel  48207  prelspr  48218  sprsymrelfolem2  48225  reupr  48254  reuopreuprim  48258  clnbgrval  48570  cycl3grtri  48695  grimgrtri  48697  usgrgrtrirex  48698  isubgr3stgrlem4  48717  isubgr3stgrlem6  48719  isubgr3stgrlem7  48720  grlimprclnbgrvtx  48747  grlimgrtri  48751  usgrexmpl1tri  48773  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  gpg3kgrtriex  48837  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5lem1  48868  pgnbgreunbgrlem5lem2  48869  pgnbgreunbgrlem5lem3  48870  pgnbgreunbgr  48873  grlimedgnedg  48879  inlinecirc02plem  49549