Theorem preq1 4690

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  preq2  4691  preq12  4692  preq1i  4693  preq1d  4696  tpeq1  4699  preq1b  4800  preq12b  4804  preq12bg  4807  prel12g  4818  elpreqpr  4821  opeq1  4839  prexOLD  5400  propeqop  5478  opthhausdorff  5489  opthhausdorff0  5490  fprg  7160  fnpr2g  7217  opthreg  9623  brdom7disj  10614  brdom6disj  10615  wunpr  10798  wunex2  10827  wuncval2  10836  grupr  10886  wwlktovf  15115  joindef  18554  meetdef  18568  pptbas  23332  usgredg4  29804  usgredg2vlem2  29813  usgredg2v  29814  nbgrval  29923  nb3grprlem2  29968  cusgredg  30011  cusgrfilem2  30043  usgredgsscusgredg  30046  rusgrnumwrdl2  30173  usgr2trlncl  30352  crctcshwlkn0lem6  30410  rusgrnumwwlks  30572  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  eupth2lem3lem4  30838  nfrgr2v  30879  frgr3vlem1  30880  frgr3vlem2  30881  3vfriswmgr  30885  3cyclfrgrrn1  30892  4cycl2vnunb  30897  vdgn1frgrv2  30903  frgrncvvdeqlem8  30913  frgrncvvdeqlem9  30914  frgrwopregasn  30923  frgrwopreglem5ALT  30929  2clwwlk2clwwlklem  30953  cplgredgex  35982  altopthsn  36819  hdmap11lem2  42993  sge0prle  47505  meadjun  47566  elsprel  48651  prelspr  48662  sprsymrelfolem2  48669  reupr  48698  reuopreuprim  48702  clnbgrval  49014  cycl3grtri  49139  grimgrtri  49141  usgrgrtrirex  49142  isubgr3stgrlem4  49161  isubgr3stgrlem6  49163  isubgr3stgrlem7  49164  grlimprclnbgrvtx  49191  grlimgrtri  49195  usgrexmpl1tri  49217  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  gpg3kgrtriex  49281  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5lem1  49312  pgnbgreunbgrlem5lem2  49313  pgnbgreunbgrlem5lem3  49314  pgnbgreunbgr  49317  grlimedgnedg  49323  inlinecirc02plem  49992