Theorem preq2 4698

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

Syntax hints:   → wi 4   = wceq 1540  {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:  preq12  4699  preq2i  4701  preq2d  4704  tpeq2  4707  ifpprsnss  4728  preq12bg  4817  prel12g  4828  elpreqprlem  4830  opeq2  4838  prex  5392  opth  5436  opeqsng  5463  propeqop  5467  relop  5814  funopg  6550  f1oprswap  6844  fprg  7127  fnprb  7182  fnpr2g  7184  prfi  9274  pr2ne  9957  pr2neOLD  9958  prdom2  9959  dfac2b  10084  brdom7disj  10484  brdom6disj  10485  wunpr  10662  wunex2  10691  wuncval2  10700  grupr  10750  prunioo  13442  hashprg  14360  wwlktovf  14922  wwlktovfo  14924  wrd2f1tovbij  14926  joindef  18335  meetdef  18349  lspfixed  21038  hmphindis  23684  upgrex  29019  edglnl  29070  usgredg4  29144  usgredgreu  29145  uspgredg2vtxeu  29147  uspgredg2v  29151  nbgrel  29267  nbupgrel  29272  nbumgrvtx  29273  nbusgreledg  29280  nbgrnself  29286  nb3grprlem1  29307  nb3grprlem2  29308  uvtxel1  29323  uvtxusgrel  29330  cusgredg  29351  usgredgsscusgredg  29387  1egrvtxdg0  29439  ifpsnprss  29551  upgriswlk  29569  uspgrn2crct  29738  wwlksnextfun  29828  wwlksnextsurj  29830  wwlksnextbij  29832  clwlkclwwlklem2  29929  clwwlkinwwlk  29969  clwwlknonex2  30038  upgr1wlkdlem1  30074  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupth2lem3lem4  30160  frcond1  30195  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  1vwmgr  30205  3vfriswmgrlem  30206  3vfriswmgr  30207  1to2vfriswmgr  30208  3cyclfrgrrn1  30214  4cycl2vnunb  30219  n4cyclfrgr  30220  vdgn1frgrv2  30225  frgrncvvdeqlem3  30230  frgrncvvdeqlem8  30235  frgrwopregbsn  30246  frgrwopreglem5ALT  30251  fusgr2wsp2nb  30263  esumpr2  34057  cplgredgex  35108  altopthsn  35949  dihprrn  41420  dvh3dim  41440  mapdindp2  41715  elsprel  47476  prelspr  47487  sprsymrelfolem2  47494  reupr  47523  reuopreuprim  47527  clnbgrel  47829  clnbupgrel  47835  sclnbgrel  47847  upgrimpths  47909  clnbgrgrim  47934  cycl3grtrilem  47945  cycl3grtri  47946  grimgrtri  47948  usgrgrtrirex  47949  stgr1  47960  stgrnbgr0  47963  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  grlimgrtri  47995  usgrexmpl1tri  48016  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpg3kgrtriex  48080  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgr  48115  upgrwlkupwlk  48128  inlinecirc02plem  48775