Theorem preq1 4582

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 4488	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4065	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4481	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4481	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1525   ∪ cun 3863  {csn 4478  {cpr 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-sn 4479  df-pr 4481

This theorem is referenced by:  preq2  4583  preq12  4584  preq1i  4585  preq1d  4588  tpeq1  4591  preq1b  4690  preq12b  4694  preq12bg  4697  prel12g  4707  elpreqpr  4710  elpr2elpr  4712  opeq1  4716  uniprg  4765  intprg  4822  prex  5231  propeqop  5295  opthhausdorff  5305  opthhausdorff0  5306  fprg  6787  fnpr2g  6846  opthreg  8934  brdom7disj  9806  brdom6disj  9807  wunpr  9984  wunex2  10013  wuncval2  10022  grupr  10072  wwlktovf  14158  joindef  17447  meetdef  17461  pptbas  21304  usgredg4  26686  usgredg2vlem2  26695  usgredg2v  26696  nbgrval  26805  nb3grprlem2  26850  cusgredg  26893  cusgrfilem2  26925  usgredgsscusgredg  26928  rusgrnumwrdl2  27055  usgr2trlncl  27227  crctcshwlkn0lem6  27279  rusgrnumwwlks  27439  upgr3v3e3cycl  27645  upgr4cycl4dv4e  27650  eupth2lem3lem4  27696  nfrgr2v  27739  frgr3vlem1  27740  frgr3vlem2  27741  3vfriswmgr  27745  3cyclfrgrrn1  27752  4cycl2vnunb  27757  vdgn1frgrv2  27763  frgrncvvdeqlem8  27773  frgrncvvdeqlem9  27774  frgrwopregasn  27783  frgrwopreglem5ALT  27789  2clwwlk2clwwlklem  27813  cplgredgex  31977  altopthsn  33033  hdmap11lem2  38530  sge0prle  42247  meadjun  42308  elsprel  43141  prelspr  43152  sprsymrelfolem2  43159  reupr  43188  reuopreuprim  43192  isomuspgrlem2d  43500  inlinecirc02plem  44276