Theorem preq1 4697

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3900  {csn 4587  {cpr 4589

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  preq2  4698  preq12  4699  preq1i  4700  preq1d  4703  tpeq1  4706  preq1b  4809  preq12b  4813  preq12bg  4816  prel12g  4827  elpreqpr  4830  opeq1  4836  prexOLD  5412  propeqop  5488  opthhausdorff  5498  opthhausdorff0  5499  fprg  7156  fnpr2g  7213  opthreg  9601  brdom7disj  10538  brdom6disj  10539  wunpr  10722  wunex2  10751  wuncval2  10760  grupr  10810  wwlktovf  15033  joindef  18468  meetdef  18482  pptbas  23239  usgredg4  29685  usgredg2vlem2  29694  usgredg2v  29695  nbgrval  29804  nb3grprlem2  29849  cusgredg  29892  cusgrfilem2  29924  usgredgsscusgredg  29927  rusgrnumwrdl2  30054  usgr2trlncl  30233  crctcshwlkn0lem6  30291  rusgrnumwwlks  30453  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  eupth2lem3lem4  30719  nfrgr2v  30760  frgr3vlem1  30761  frgr3vlem2  30762  3vfriswmgr  30766  3cyclfrgrrn1  30773  4cycl2vnunb  30778  vdgn1frgrv2  30784  frgrncvvdeqlem8  30794  frgrncvvdeqlem9  30795  frgrwopregasn  30804  frgrwopreglem5ALT  30810  2clwwlk2clwwlklem  30834  cplgredgex  35727  altopthsn  36549  hdmap11lem2  42723  sge0prle  47237  meadjun  47298  elsprel  48383  prelspr  48394  sprsymrelfolem2  48401  reupr  48430  reuopreuprim  48434  clnbgrval  48746  cycl3grtri  48871  grimgrtri  48873  usgrgrtrirex  48874  isubgr3stgrlem4  48893  isubgr3stgrlem6  48895  isubgr3stgrlem7  48896  grlimprclnbgrvtx  48923  grlimgrtri  48927  usgrexmpl1tri  48949  gpg5nbgrvtx03star  49004  gpg5nbgr3star  49005  gpg3kgrtriex  49013  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  pgnbgreunbgr  49049  grlimedgnedg  49055  inlinecirc02plem  49724