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 4169	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4591	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4591	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 4152  {csn 4588  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  preq2  4695  preq12  4696  preq1i  4697  preq1d  4700  tpeq1  4703  preq1b  4804  preq12b  4808  preq12bg  4811  prel12g  4822  elpreqpr  4825  opeq1  4843  prexOLD  5406  propeqop  5484  opthhausdorff  5495  opthhausdorff0  5496  fprg  7186  fnpr2g  7242  opthreg  9649  brdom7disj  10640  brdom6disj  10641  wunpr  10824  wunex2  10853  wuncval2  10862  grupr  10912  wwlktovf  15141  joindef  18580  meetdef  18594  pptbas  23359  usgredg4  29831  usgredg2vlem2  29840  usgredg2v  29841  nbgrval  29950  nb3grprlem2  29995  cusgredg  30038  cusgrfilem2  30070  usgredgsscusgredg  30073  rusgrnumwrdl2  30200  usgr2trlncl  30379  crctcshwlkn0lem6  30437  rusgrnumwwlks  30599  upgr3v3e3cycl  30814  upgr4cycl4dv4e  30819  eupth2lem3lem4  30865  nfrgr2v  30906  frgr3vlem1  30907  frgr3vlem2  30908  3vfriswmgr  30912  3cyclfrgrrn1  30919  4cycl2vnunb  30924  vdgn1frgrv2  30930  frgrncvvdeqlem8  30940  frgrncvvdeqlem9  30941  frgrwopregasn  30950  frgrwopreglem5ALT  30956  2clwwlk2clwwlklem  30980  gdlop1fv  35976  cplgredgex  36075  altopthsn  36917  hdmap11lem2  43102  sge0prle  47626  meadjun  47687  elsprel  48772  prelspr  48783  sprsymrelfolem2  48790  reupr  48819  reuopreuprim  48823  clnbgrval  49135  cycl3grtri  49260  grimgrtri  49262  usgrgrtrirex  49263  isubgr3stgrlem4  49282  isubgr3stgrlem6  49284  isubgr3stgrlem7  49285  grlimprclnbgrvtx  49312  grlimgrtri  49316  usgrexmpl1tri  49338  gpg5nbgrvtx03star  49393  gpg5nbgr3star  49394  gpg3kgrtriex  49402  pgnbgreunbgrlem1  49426  pgnbgreunbgrlem2lem1  49427  pgnbgreunbgrlem2lem2  49428  pgnbgreunbgrlem2lem3  49429  pgnbgreunbgrlem4  49432  pgnbgreunbgrlem5lem1  49433  pgnbgreunbgrlem5lem2  49434  pgnbgreunbgrlem5lem3  49435  pgnbgreunbgr  49438  grlimedgnedg  49444  inlinecirc02plem  50113