Theorem preq2 4759

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 4758	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2		prcom 4757	. 2 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
3		prcom 4757	. 2 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
4	1, 2, 3	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1537  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  preq12  4760  preq2i  4762  preq2d  4765  tpeq2  4768  ifpprsnss  4789  preq12bg  4878  prel12g  4888  elpreqprlem  4890  opeq2  4898  prex  5452  opth  5496  opeqsng  5522  propeqop  5526  relop  5875  funopg  6612  f1oprswap  6906  fprg  7189  fnprb  7245  fnpr2g  7247  prfi  9391  pr2ne  10073  pr2neOLD  10074  prdom2  10075  dfac2b  10200  brdom7disj  10600  brdom6disj  10601  wunpr  10778  wunex2  10807  wuncval2  10816  grupr  10866  prunioo  13541  hashprg  14444  wwlktovf  15005  wwlktovfo  15007  wrd2f1tovbij  15009  joindef  18446  meetdef  18460  lspfixed  21153  hmphindis  23826  upgrex  29127  edglnl  29178  usgredg4  29252  usgredgreu  29253  uspgredg2vtxeu  29255  uspgredg2v  29259  nbgrel  29375  nbupgrel  29380  nbumgrvtx  29381  nbusgreledg  29388  nbgrnself  29394  nb3grprlem1  29415  nb3grprlem2  29416  uvtxel1  29431  uvtxusgrel  29438  cusgredg  29459  usgredgsscusgredg  29495  1egrvtxdg0  29547  ifpsnprss  29659  upgriswlk  29677  uspgrn2crct  29841  wwlksnextfun  29931  wwlksnextsurj  29933  wwlksnextbij  29935  clwlkclwwlklem2  30032  clwwlkinwwlk  30072  clwwlknonex2  30141  upgr1wlkdlem1  30177  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2lem3lem4  30263  frcond1  30298  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  1vwmgr  30308  3vfriswmgrlem  30309  3vfriswmgr  30310  1to2vfriswmgr  30311  3cyclfrgrrn1  30317  4cycl2vnunb  30322  n4cyclfrgr  30323  vdgn1frgrv2  30328  frgrncvvdeqlem3  30333  frgrncvvdeqlem8  30338  frgrwopregbsn  30349  frgrwopreglem5ALT  30354  fusgr2wsp2nb  30366  esumpr2  34031  cplgredgex  35088  altopthsn  35925  dihprrn  41383  dvh3dim  41403  mapdindp2  41678  elsprel  47349  prelspr  47360  sprsymrelfolem2  47367  reupr  47396  reuopreuprim  47400  clnbgrel  47701  clnbupgrel  47707  sclnbgrel  47719  clnbgrgrim  47786  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  usgrexmpl1tri  47840  upgrwlkupwlk  47863  inlinecirc02plem  48520