Theorem preq1 4697

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 4599	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	uneq1d 4130	. 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3		df-pr 4592	. 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4		df-pr 4592	. 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3912  {csn 4589  {cpr 4591

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  preq2  4698  preq12  4699  preq1i  4700  preq1d  4703  tpeq1  4706  preq1b  4810  preq12b  4814  preq12bg  4817  prel12g  4828  elpreqpr  4831  opeq1  4837  prex  5392  propeqop  5467  opthhausdorff  5477  opthhausdorff0  5478  fprg  7127  fnpr2g  7184  opthreg  9571  brdom7disj  10484  brdom6disj  10485  wunpr  10662  wunex2  10691  wuncval2  10700  grupr  10750  wwlktovf  14922  joindef  18335  meetdef  18349  pptbas  22895  usgredg4  29144  usgredg2vlem2  29153  usgredg2v  29154  nbgrval  29263  nb3grprlem2  29308  cusgredg  29351  cusgrfilem2  29384  usgredgsscusgredg  29387  rusgrnumwrdl2  29514  usgr2trlncl  29690  crctcshwlkn0lem6  29745  rusgrnumwwlks  29904  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupth2lem3lem4  30160  nfrgr2v  30201  frgr3vlem1  30202  frgr3vlem2  30203  3vfriswmgr  30207  3cyclfrgrrn1  30214  4cycl2vnunb  30219  vdgn1frgrv2  30225  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  frgrwopregasn  30245  frgrwopreglem5ALT  30251  2clwwlk2clwwlklem  30275  cplgredgex  35108  altopthsn  35949  hdmap11lem2  41836  sge0prle  46399  meadjun  46460  elsprel  47476  prelspr  47487  sprsymrelfolem2  47494  reupr  47523  reuopreuprim  47527  clnbgrval  47823  cycl3grtri  47946  grimgrtri  47948  usgrgrtrirex  47949  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  grlimgrtri  47995  usgrexmpl1tri  48016  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpg3kgrtriex  48080  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgr  48115  inlinecirc02plem  48775