Theorem preq1 4704

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 4604	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4124	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4597	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4597	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2826	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3906  {csn 4594  {cpr 4596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  preq2  4705  preq12  4706  preq1i  4707  preq1d  4710  tpeq1  4713  preq1b  4816  preq12b  4820  preq12bg  4823  prel12g  4834  elpreqpr  4837  opeq1  4843  prexOLD  5419  propeqop  5495  opthhausdorff  5505  opthhausdorff0  5506  fprg  7159  fnpr2g  7215  opthreg  9597  brdom7disj  10533  brdom6disj  10534  wunpr  10712  wunex2  10741  wuncval2  10750  grupr  10800  wwlktovf  15019  joindef  18455  meetdef  18469  pptbas  23202  usgredg4  29604  usgredg2vlem2  29613  usgredg2v  29614  nbgrval  29723  nb3grprlem2  29768  cusgredg  29811  cusgrfilem2  29843  usgredgsscusgredg  29846  rusgrnumwrdl2  29973  usgr2trlncl  30146  crctcshwlkn0lem6  30201  rusgrnumwwlks  30363  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  eupth2lem3lem4  30619  nfrgr2v  30660  frgr3vlem1  30661  frgr3vlem2  30662  3vfriswmgr  30666  3cyclfrgrrn1  30673  4cycl2vnunb  30678  vdgn1frgrv2  30684  frgrncvvdeqlem8  30694  frgrncvvdeqlem9  30695  frgrwopregasn  30704  frgrwopreglem5ALT  30710  2clwwlk2clwwlklem  30734  cplgredgex  35634  altopthsn  36474  hdmap11lem2  42657  sge0prle  47156  meadjun  47217  elsprel  48265  prelspr  48276  sprsymrelfolem2  48283  reupr  48312  reuopreuprim  48316  clnbgrval  48628  cycl3grtri  48753  grimgrtri  48755  usgrgrtrirex  48756  isubgr3stgrlem4  48775  isubgr3stgrlem6  48777  isubgr3stgrlem7  48778  grlimprclnbgrvtx  48805  grlimgrtri  48809  usgrexmpl1tri  48831  gpg5nbgrvtx03star  48886  gpg5nbgr3star  48887  gpg3kgrtriex  48895  pgnbgreunbgrlem1  48919  pgnbgreunbgrlem2lem1  48920  pgnbgreunbgrlem2lem2  48921  pgnbgreunbgrlem2lem3  48922  pgnbgreunbgrlem4  48925  pgnbgreunbgrlem5lem1  48926  pgnbgreunbgrlem5lem2  48927  pgnbgreunbgrlem5lem3  48928  pgnbgreunbgr  48931  grlimedgnedg  48937  inlinecirc02plem  49607