Theorem preq1 4672

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 4572	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4104	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4565	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4565	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2800	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1547   ∪ cun 3888  {csn 4562  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  preq2  4673  preq12  4674  preq1i  4675  preq1d  4678  tpeq1  4681  preq1b  4784  preq12b  4788  preq12bg  4791  prel12g  4802  elpreqpr  4805  opeq1  4811  prexOLD  5379  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  fprg  7105  fnpr2g  7161  opthreg  9537  brdom7disj  10451  brdom6disj  10452  wunpr  10630  wunex2  10659  wuncval2  10668  grupr  10718  wwlktovf  14916  joindef  18338  meetdef  18352  pptbas  22998  usgredg4  29311  usgredg2vlem2  29320  usgredg2v  29321  nbgrval  29430  nb3grprlem2  29475  cusgredg  29518  cusgrfilem2  29550  usgredgsscusgredg  29553  rusgrnumwrdl2  29680  usgr2trlncl  29853  crctcshwlkn0lem6  29908  rusgrnumwwlks  30070  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eupth2lem3lem4  30326  nfrgr2v  30367  frgr3vlem1  30368  frgr3vlem2  30369  3vfriswmgr  30373  3cyclfrgrrn1  30380  4cycl2vnunb  30385  vdgn1frgrv2  30391  frgrncvvdeqlem8  30401  frgrncvvdeqlem9  30402  frgrwopregasn  30411  frgrwopreglem5ALT  30417  2clwwlk2clwwlklem  30441  cplgredgex  35356  altopthsn  36196  hdmap11lem2  42341  sge0prle  46851  meadjun  46912  elsprel  47957  prelspr  47968  sprsymrelfolem2  47975  reupr  48004  reuopreuprim  48008  clnbgrval  48320  cycl3grtri  48445  grimgrtri  48447  usgrgrtrirex  48448  isubgr3stgrlem4  48467  isubgr3stgrlem6  48469  isubgr3stgrlem7  48470  grlimprclnbgrvtx  48497  grlimgrtri  48501  usgrexmpl1tri  48523  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  gpg3kgrtriex  48587  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  pgnbgreunbgr  48623  grlimedgnedg  48629  inlinecirc02plem  49284