Theorem preq1 4687

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 4587	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4116	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4580	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4580	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3896  {csn 4577  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  preq2  4688  preq12  4689  preq1i  4690  preq1d  4693  tpeq1  4696  preq1b  4799  preq12b  4803  preq12bg  4806  prel12g  4817  elpreqpr  4820  opeq1  4826  prex  5379  propeqop  5452  opthhausdorff  5462  opthhausdorff0  5463  fprg  7096  fnpr2g  7152  opthreg  9517  brdom7disj  10431  brdom6disj  10432  wunpr  10609  wunex2  10638  wuncval2  10647  grupr  10697  wwlktovf  14867  joindef  18284  meetdef  18298  pptbas  22926  usgredg4  29199  usgredg2vlem2  29208  usgredg2v  29209  nbgrval  29318  nb3grprlem2  29363  cusgredg  29406  cusgrfilem2  29439  usgredgsscusgredg  29442  rusgrnumwrdl2  29569  usgr2trlncl  29742  crctcshwlkn0lem6  29797  rusgrnumwwlks  29959  upgr3v3e3cycl  30164  upgr4cycl4dv4e  30169  eupth2lem3lem4  30215  nfrgr2v  30256  frgr3vlem1  30257  frgr3vlem2  30258  3vfriswmgr  30262  3cyclfrgrrn1  30269  4cycl2vnunb  30274  vdgn1frgrv2  30280  frgrncvvdeqlem8  30290  frgrncvvdeqlem9  30291  frgrwopregasn  30300  frgrwopreglem5ALT  30306  2clwwlk2clwwlklem  30330  cplgredgex  35188  altopthsn  36028  hdmap11lem2  41964  sge0prle  46526  meadjun  46587  elsprel  47602  prelspr  47613  sprsymrelfolem2  47620  reupr  47649  reuopreuprim  47653  clnbgrval  47949  cycl3grtri  48074  grimgrtri  48076  usgrgrtrirex  48077  isubgr3stgrlem4  48096  isubgr3stgrlem6  48098  isubgr3stgrlem7  48099  grlimprclnbgrvtx  48126  grlimgrtri  48130  usgrexmpl1tri  48152  gpg5nbgrvtx03star  48207  gpg5nbgr3star  48208  gpg3kgrtriex  48216  pgnbgreunbgrlem1  48240  pgnbgreunbgrlem2lem1  48241  pgnbgreunbgrlem2lem2  48242  pgnbgreunbgrlem2lem3  48243  pgnbgreunbgrlem4  48246  pgnbgreunbgrlem5lem1  48247  pgnbgreunbgrlem5lem2  48248  pgnbgreunbgrlem5lem3  48249  pgnbgreunbgr  48252  grlimedgnedg  48258  inlinecirc02plem  48914