Theorem preq1 4694

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3897  {csn 4584  {cpr 4586

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  preq2  4695  preq12  4696  preq1i  4697  preq1d  4700  tpeq1  4703  preq1b  4806  preq12b  4810  preq12bg  4813  prel12g  4824  elpreqpr  4827  opeq1  4833  prexOLD  5401  propeqop  5479  opthhausdorff  5490  opthhausdorff0  5491  fprg  7151  fnpr2g  7208  opthreg  9603  brdom7disj  10591  brdom6disj  10592  wunpr  10775  wunex2  10804  wuncval2  10813  grupr  10863  wwlktovf  15089  joindef  18528  meetdef  18542  pptbas  23306  usgredg4  29780  usgredg2vlem2  29789  usgredg2v  29790  nbgrval  29899  nb3grprlem2  29944  cusgredg  29987  cusgrfilem2  30019  usgredgsscusgredg  30022  rusgrnumwrdl2  30149  usgr2trlncl  30328  crctcshwlkn0lem6  30386  rusgrnumwwlks  30548  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  eupth2lem3lem4  30814  nfrgr2v  30855  frgr3vlem1  30856  frgr3vlem2  30857  3vfriswmgr  30861  3cyclfrgrrn1  30868  4cycl2vnunb  30873  vdgn1frgrv2  30879  frgrncvvdeqlem8  30889  frgrncvvdeqlem9  30890  frgrwopregasn  30899  frgrwopreglem5ALT  30905  2clwwlk2clwwlklem  30929  cplgredgex  35874  altopthsn  36696  hdmap11lem2  42867  sge0prle  47355  meadjun  47416  elsprel  48501  prelspr  48512  sprsymrelfolem2  48519  reupr  48548  reuopreuprim  48552  clnbgrval  48864  cycl3grtri  48989  grimgrtri  48991  usgrgrtrirex  48992  isubgr3stgrlem4  49011  isubgr3stgrlem6  49013  isubgr3stgrlem7  49014  grlimprclnbgrvtx  49041  grlimgrtri  49045  usgrexmpl1tri  49067  gpg5nbgrvtx03star  49122  gpg5nbgr3star  49123  gpg3kgrtriex  49131  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem4  49161  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  pgnbgreunbgr  49167  grlimedgnedg  49173  inlinecirc02plem  49842