Theorem preq1 4212

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 4135	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 3728	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4128	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4128	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1475   ∪ cun 3538  {csn 4125  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  preq2  4213  preq12  4214  preq1i  4215  preq1d  4218  tpeq1  4221  prnzgOLD  4255  preq1b  4317  preq12b  4322  preq12bg  4326  prel12g  4327  elpreqpr  4334  elpr2elpr  4336  opeq1  4340  uniprg  4386  intprg  4446  prex  4836  propeqop  4895  fprg  6327  fnpr2g  6379  opthreg  8398  brdom7disj  9234  brdom6disj  9235  wunpr  9410  wunex2  9439  wuncval2  9448  grupr  9498  wwlktovf  13547  joindef  16827  meetdef  16841  pptbas  20622  upgredg  25811  usgraedg4  25916  usgraidx2vlem2  25921  usgraidx2v  25922  nbgraop  25952  nb3graprlem2  25981  cusgrarn  25988  cusgra2v  25991  nbcusgra  25992  cusgra3v  25993  cusgrafilem2  26008  usgrasscusgra  26011  uvtxnbgra  26021  usgra2wlkspthlem1  26147  usgrcyclnl2  26169  4cycl4dv  26195  usg2spthonot0  26416  rusgraprop4  26471  rusgrasn  26472  rusgranumwwlkl1  26473  rusgranumwlks  26483  frgra2v  26526  frgra3vlem1  26527  frgra3vlem2  26528  3vfriswmgra  26532  3cyclfrgrarn1  26539  4cycl2vnunb  26544  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  frgrawopreglem5  26575  frgrawopreg1  26577  frgraregorufr0  26579  frg2woteqm  26586  usg2spot2nb  26592  extwwlkfablem1  26601  altopthsn  31238  hdmap11lem2  36152  sge0prle  39294  meadjun  39355  usgredg4  40444  usgredg2vlem2  40453  usgredg2v  40454  nbgrval  40560  nb3grprlem2  40609  cusgredg  40646  cusgrfilem2  40672  usgredgsscusgredg  40675  rusgrnumwrdl2  40786  usgr2trlncl  40966  crctcsh1wlkn0lem6  41018  rusgrnumwwlks  41177  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupth2lem3lem4  41399  nfrgr2v  41442  frgr3vlem1  41443  frgr3vlem2  41444  3vfriswmgr  41448  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  vdgn1frgrv2  41466  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  frgrwopreglem5  41485  frgrwopreg1  41487  frgrregorufr0  41489  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498