Theorem preq1 4733

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 4636	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4167	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4629	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4629	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3949  {csn 4626  {cpr 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  preq2  4734  preq12  4735  preq1i  4736  preq1d  4739  tpeq1  4742  preq1b  4846  preq12b  4850  preq12bg  4853  prel12g  4864  elpreqpr  4867  opeq1  4873  prex  5437  propeqop  5512  opthhausdorff  5522  opthhausdorff0  5523  fprg  7175  fnpr2g  7230  opthreg  9658  brdom7disj  10571  brdom6disj  10572  wunpr  10749  wunex2  10778  wuncval2  10787  grupr  10837  wwlktovf  14995  joindef  18421  meetdef  18435  pptbas  23015  usgredg4  29234  usgredg2vlem2  29243  usgredg2v  29244  nbgrval  29353  nb3grprlem2  29398  cusgredg  29441  cusgrfilem2  29474  usgredgsscusgredg  29477  rusgrnumwrdl2  29604  usgr2trlncl  29780  crctcshwlkn0lem6  29835  rusgrnumwwlks  29994  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth2lem3lem4  30250  nfrgr2v  30291  frgr3vlem1  30292  frgr3vlem2  30293  3vfriswmgr  30297  3cyclfrgrrn1  30304  4cycl2vnunb  30309  vdgn1frgrv2  30315  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  frgrwopregasn  30335  frgrwopreglem5ALT  30341  2clwwlk2clwwlklem  30365  cplgredgex  35126  altopthsn  35962  hdmap11lem2  41844  sge0prle  46416  meadjun  46477  elsprel  47462  prelspr  47473  sprsymrelfolem2  47480  reupr  47509  reuopreuprim  47513  clnbgrval  47809  cycl3grtri  47914  grimgrtri  47916  usgrgrtrirex  47917  isubgr3stgrlem4  47936  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  grlimgrtri  47963  usgrexmpl1tri  47984  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpg3kgrtriex  48045  inlinecirc02plem  48707