Theorem preq1 4737

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 4640	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4176	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4633	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4633	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1536   ∪ cun 3960  {csn 4630  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-pr 4633

This theorem is referenced by:  preq2  4738  preq12  4739  preq1i  4740  preq1d  4743  tpeq1  4746  preq1b  4850  preq12b  4854  preq12bg  4857  prel12g  4868  elpreqpr  4871  opeq1  4877  prex  5442  propeqop  5516  opthhausdorff  5526  opthhausdorff0  5527  fprg  7174  fnpr2g  7229  opthreg  9655  brdom7disj  10568  brdom6disj  10569  wunpr  10746  wunex2  10775  wuncval2  10784  grupr  10834  wwlktovf  14991  joindef  18433  meetdef  18447  pptbas  23030  usgredg4  29248  usgredg2vlem2  29257  usgredg2v  29258  nbgrval  29367  nb3grprlem2  29412  cusgredg  29455  cusgrfilem2  29488  usgredgsscusgredg  29491  rusgrnumwrdl2  29618  usgr2trlncl  29792  crctcshwlkn0lem6  29844  rusgrnumwwlks  30003  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2lem3lem4  30259  nfrgr2v  30300  frgr3vlem1  30301  frgr3vlem2  30302  3vfriswmgr  30306  3cyclfrgrrn1  30313  4cycl2vnunb  30318  vdgn1frgrv2  30324  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  frgrwopregasn  30344  frgrwopreglem5ALT  30350  2clwwlk2clwwlklem  30374  cplgredgex  35104  altopthsn  35942  hdmap11lem2  41824  sge0prle  46356  meadjun  46417  elsprel  47399  prelspr  47410  sprsymrelfolem2  47417  reupr  47446  reuopreuprim  47450  clnbgrval  47746  grimgrtri  47851  usgrgrtrirex  47852  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  grlimgrtri  47898  usgrexmpl1tri  47919  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  inlinecirc02plem  48635