Theorem preq1 4692

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3901  {csn 4582  {cpr 4584

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 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  preq2  4693  preq12  4694  preq1i  4695  preq1d  4698  tpeq1  4701  preq1b  4804  preq12b  4808  preq12bg  4811  prel12g  4822  elpreqpr  4825  opeq1  4831  prexOLD  5389  propeqop  5463  opthhausdorff  5473  opthhausdorff0  5474  fprg  7110  fnpr2g  7166  opthreg  9539  brdom7disj  10453  brdom6disj  10454  wunpr  10632  wunex2  10661  wuncval2  10670  grupr  10720  wwlktovf  14891  joindef  18309  meetdef  18323  pptbas  22964  usgredg4  29302  usgredg2vlem2  29311  usgredg2v  29312  nbgrval  29421  nb3grprlem2  29466  cusgredg  29509  cusgrfilem2  29542  usgredgsscusgredg  29545  rusgrnumwrdl2  29672  usgr2trlncl  29845  crctcshwlkn0lem6  29900  rusgrnumwwlks  30062  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eupth2lem3lem4  30318  nfrgr2v  30359  frgr3vlem1  30360  frgr3vlem2  30361  3vfriswmgr  30365  3cyclfrgrrn1  30372  4cycl2vnunb  30377  vdgn1frgrv2  30383  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  frgrwopregasn  30403  frgrwopreglem5ALT  30409  2clwwlk2clwwlklem  30433  cplgredgex  35334  altopthsn  36174  hdmap11lem2  42215  sge0prle  46756  meadjun  46817  elsprel  47832  prelspr  47843  sprsymrelfolem2  47850  reupr  47879  reuopreuprim  47883  clnbgrval  48179  cycl3grtri  48304  grimgrtri  48306  usgrgrtrirex  48307  isubgr3stgrlem4  48326  isubgr3stgrlem6  48328  isubgr3stgrlem7  48329  grlimprclnbgrvtx  48356  grlimgrtri  48360  usgrexmpl1tri  48382  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  gpg3kgrtriex  48446  pgnbgreunbgrlem1  48470  pgnbgreunbgrlem2lem1  48471  pgnbgreunbgrlem2lem2  48472  pgnbgreunbgrlem2lem3  48473  pgnbgreunbgrlem4  48476  pgnbgreunbgrlem5lem1  48477  pgnbgreunbgrlem5lem2  48478  pgnbgreunbgrlem5lem3  48479  pgnbgreunbgr  48482  grlimedgnedg  48488  inlinecirc02plem  49143