Theorem preq2 4630

Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
preq2	⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2

Step	Hyp	Ref	Expression
1		preq1 4629	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2		prcom 4628	. 2 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
3		prcom 4628	. 2 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
4	1, 2, 3	3eqtr4g 2818	1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1538  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-sn 4526  df-pr 4528

This theorem is referenced by:  preq12  4631  preq2i  4633  preq2d  4636  tpeq2  4639  ifpprsnss  4660  preq12bg  4744  prel12g  4754  elpreqprlem  4756  elpr2elpr  4759  opeq2  4766  opeq2OLD  4767  uniprgOLD  4821  intprgOLD  4877  prex  5305  opth  5340  opeqsng  5366  propeqop  5370  relop  5696  funopg  6374  f1oprswap  6650  fprg  6914  fnprb  6968  fnpr2g  6970  pr2ne  9478  prdom2  9479  dfac2b  9603  brdom7disj  10004  brdom6disj  10005  wunpr  10182  wunex2  10211  wuncval2  10220  grupr  10270  prunioo  12926  hashprg  13819  wwlktovf  14380  wwlktovfo  14382  wrd2f1tovbij  14384  joindef  17693  meetdef  17707  lspfixed  19981  hmphindis  22510  upgrex  26997  edglnl  27048  usgredg4  27119  usgredgreu  27120  uspgredg2vtxeu  27122  uspgredg2v  27126  nbgrel  27242  nbupgrel  27247  nbumgrvtx  27248  nbusgreledg  27255  nbgrnself  27261  nb3grprlem1  27282  nb3grprlem2  27283  uvtxel1  27298  uvtxusgrel  27305  cusgredg  27326  usgredgsscusgredg  27361  1egrvtxdg0  27413  ifpsnprss  27524  upgriswlk  27542  uspgrn2crct  27706  wwlksnextfun  27796  wwlksnextsurj  27798  wwlksnextbij  27800  clwlkclwwlklem2  27897  clwwlkinwwlk  27937  clwwlknonex2  28006  upgr1wlkdlem1  28042  upgr3v3e3cycl  28077  upgr4cycl4dv4e  28082  eupth2lem3lem4  28128  frcond1  28163  frgr1v  28168  nfrgr2v  28169  frgr3v  28172  1vwmgr  28173  3vfriswmgrlem  28174  3vfriswmgr  28175  1to2vfriswmgr  28176  3cyclfrgrrn1  28182  4cycl2vnunb  28187  n4cyclfrgr  28188  vdgn1frgrv2  28193  frgrncvvdeqlem3  28198  frgrncvvdeqlem8  28203  frgrwopregbsn  28214  frgrwopreglem5ALT  28219  fusgr2wsp2nb  28231  esumpr2  31566  cplgredgex  32610  altopthsn  33846  dihprrn  39036  dvh3dim  39056  mapdindp2  39331  elsprel  44409  prelspr  44420  sprsymrelfolem2  44427  reupr  44456  reuopreuprim  44460  isomuspgrlem2d  44765  upgrwlkupwlk  44784  inlinecirc02plem  45614