Theorem preq2 4694

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4587

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 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  preq12  4695  preq2i  4697  preq2d  4700  tpeq2  4703  ifpprsnss  4724  preq12bg  4813  prel12g  4824  elpreqprlem  4826  opeq2  4834  prex  5387  opth  5431  opeqsng  5458  propeqop  5462  relop  5804  funopg  6534  f1oprswap  6826  fprg  7109  fnprb  7164  fnpr2g  7166  prfi  9250  pr2ne  9933  pr2neOLD  9934  prdom2  9935  dfac2b  10060  brdom7disj  10460  brdom6disj  10461  wunpr  10638  wunex2  10667  wuncval2  10676  grupr  10726  prunioo  13418  hashprg  14336  wwlktovf  14898  wwlktovfo  14900  wrd2f1tovbij  14902  joindef  18311  meetdef  18325  lspfixed  21014  hmphindis  23660  upgrex  28995  edglnl  29046  usgredg4  29120  usgredgreu  29121  uspgredg2vtxeu  29123  uspgredg2v  29127  nbgrel  29243  nbupgrel  29248  nbumgrvtx  29249  nbusgreledg  29256  nbgrnself  29262  nb3grprlem1  29283  nb3grprlem2  29284  uvtxel1  29299  uvtxusgrel  29306  cusgredg  29327  usgredgsscusgredg  29363  1egrvtxdg0  29415  ifpsnprss  29526  upgriswlk  29544  uspgrn2crct  29711  wwlksnextfun  29801  wwlksnextsurj  29803  wwlksnextbij  29805  clwlkclwwlklem2  29902  clwwlkinwwlk  29942  clwwlknonex2  30011  upgr1wlkdlem1  30047  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  eupth2lem3lem4  30133  frcond1  30168  frgr1v  30173  nfrgr2v  30174  frgr3v  30177  1vwmgr  30178  3vfriswmgrlem  30179  3vfriswmgr  30180  1to2vfriswmgr  30181  3cyclfrgrrn1  30187  4cycl2vnunb  30192  n4cyclfrgr  30193  vdgn1frgrv2  30198  frgrncvvdeqlem3  30203  frgrncvvdeqlem8  30208  frgrwopregbsn  30219  frgrwopreglem5ALT  30224  fusgr2wsp2nb  30236  esumpr2  34030  cplgredgex  35081  altopthsn  35922  dihprrn  41393  dvh3dim  41413  mapdindp2  41688  elsprel  47449  prelspr  47460  sprsymrelfolem2  47467  reupr  47496  reuopreuprim  47500  clnbgrel  47802  clnbupgrel  47808  sclnbgrel  47820  upgrimpths  47882  clnbgrgrim  47907  cycl3grtrilem  47918  cycl3grtri  47919  grimgrtri  47921  usgrgrtrirex  47922  stgr1  47933  stgrnbgr0  47936  isubgr3stgrlem4  47941  isubgr3stgrlem6  47943  grlimgrtri  47968  usgrexmpl1tri  47989  gpgnbgrvtx0  48038  gpgnbgrvtx1  48039  gpg5nbgrvtx03star  48044  gpg5nbgr3star  48045  gpg3kgrtriex  48053  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  pgnbgreunbgr  48088  upgrwlkupwlk  48101  inlinecirc02plem  48748