Theorem preq1 4738

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 4639	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4163	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4632	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4632	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3947  {csn 4629  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  preq2  4739  preq12  4740  preq1i  4741  preq1d  4744  tpeq1  4747  preq1b  4848  preq12b  4852  preq12bg  4855  prel12g  4865  elpreqpr  4868  elpr2elpr  4870  opeq1  4874  uniprgOLD  4929  intprgOLD  4989  prex  5433  propeqop  5508  opthhausdorff  5518  opthhausdorff0  5519  fprg  7153  fnpr2g  7212  opthreg  9613  brdom7disj  10526  brdom6disj  10527  wunpr  10704  wunex2  10733  wuncval2  10742  grupr  10792  wwlktovf  14907  joindef  18329  meetdef  18343  pptbas  22511  usgredg4  28474  usgredg2vlem2  28483  usgredg2v  28484  nbgrval  28593  nb3grprlem2  28638  cusgredg  28681  cusgrfilem2  28713  usgredgsscusgredg  28716  rusgrnumwrdl2  28843  usgr2trlncl  29017  crctcshwlkn0lem6  29069  rusgrnumwwlks  29228  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupth2lem3lem4  29484  nfrgr2v  29525  frgr3vlem1  29526  frgr3vlem2  29527  3vfriswmgr  29531  3cyclfrgrrn1  29538  4cycl2vnunb  29543  vdgn1frgrv2  29549  frgrncvvdeqlem8  29559  frgrncvvdeqlem9  29560  frgrwopregasn  29569  frgrwopreglem5ALT  29575  2clwwlk2clwwlklem  29599  cplgredgex  34111  altopthsn  34933  hdmap11lem2  40713  sge0prle  45117  meadjun  45178  elsprel  46143  prelspr  46154  sprsymrelfolem2  46161  reupr  46190  reuopreuprim  46194  isomuspgrlem2d  46499  inlinecirc02plem  47472