Theorem preq1 4700

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 4602	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4133	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4595	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4595	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3915  {csn 4592  {cpr 4594

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  preq2  4701  preq12  4702  preq1i  4703  preq1d  4706  tpeq1  4709  preq1b  4813  preq12b  4817  preq12bg  4820  prel12g  4831  elpreqpr  4834  opeq1  4840  prex  5395  propeqop  5470  opthhausdorff  5480  opthhausdorff0  5481  fprg  7130  fnpr2g  7187  opthreg  9578  brdom7disj  10491  brdom6disj  10492  wunpr  10669  wunex2  10698  wuncval2  10707  grupr  10757  wwlktovf  14929  joindef  18342  meetdef  18356  pptbas  22902  usgredg4  29151  usgredg2vlem2  29160  usgredg2v  29161  nbgrval  29270  nb3grprlem2  29315  cusgredg  29358  cusgrfilem2  29391  usgredgsscusgredg  29394  rusgrnumwrdl2  29521  usgr2trlncl  29697  crctcshwlkn0lem6  29752  rusgrnumwwlks  29911  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eupth2lem3lem4  30167  nfrgr2v  30208  frgr3vlem1  30209  frgr3vlem2  30210  3vfriswmgr  30214  3cyclfrgrrn1  30221  4cycl2vnunb  30226  vdgn1frgrv2  30232  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  frgrwopregasn  30252  frgrwopreglem5ALT  30258  2clwwlk2clwwlklem  30282  cplgredgex  35115  altopthsn  35956  hdmap11lem2  41843  sge0prle  46406  meadjun  46467  elsprel  47480  prelspr  47491  sprsymrelfolem2  47498  reupr  47527  reuopreuprim  47531  clnbgrval  47827  cycl3grtri  47950  grimgrtri  47952  usgrgrtrirex  47953  isubgr3stgrlem4  47972  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  grlimgrtri  47999  usgrexmpl1tri  48020  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpg3kgrtriex  48084  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgr  48119  inlinecirc02plem  48779