Theorem preq2 4581

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

Syntax hints:   → wi 4   = wceq 1522  {cpr 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3868  df-sn 4477  df-pr 4479

This theorem is referenced by:  preq12  4582  preq2i  4584  preq2d  4587  tpeq2  4590  ifpprsnss  4611  preq12bg  4695  prel12g  4705  elpreqprlem  4707  elpr2elpr  4710  opeq2  4715  uniprg  4763  intprg  4820  prex  5229  opth  5265  opeqsng  5289  propeqop  5293  relop  5612  funopg  6264  f1oprswap  6531  fprg  6785  fnprb  6842  fnpr2g  6844  pr2ne  9282  prdom2  9283  dfac2b  9407  brdom7disj  9804  brdom6disj  9805  wunpr  9982  wunex2  10011  wuncval2  10020  grupr  10070  prunioo  12722  hashprg  13609  wwlktovf  14159  wwlktovfo  14161  wrd2f1tovbij  14163  joindef  17448  meetdef  17462  lspfixed  19595  hmphindis  22094  upgrex  26565  edglnl  26616  usgredg4  26687  usgredgreu  26688  uspgredg2vtxeu  26690  uspgredg2v  26694  nbgrel  26810  nbupgrel  26815  nbumgrvtx  26816  nbusgreledg  26823  nbgrnself  26829  nb3grprlem1  26850  nb3grprlem2  26851  uvtxel1  26866  uvtxusgrel  26873  cusgredg  26894  usgredgsscusgredg  26929  1egrvtxdg0  26981  ifpsnprss  27092  upgriswlk  27110  uspgrn2crct  27278  wwlksnextfun  27368  wwlksnextsurj  27370  wwlksnextbij  27372  clwlkclwwlklem2  27470  clwwlkinwwlk  27510  clwwlknonex2  27580  upgr1wlkdlem1  27616  upgr3v3e3cycl  27651  upgr4cycl4dv4e  27656  eupth2lem3lem4  27703  frcond1  27742  frgr1v  27747  nfrgr2v  27748  frgr3v  27751  1vwmgr  27752  3vfriswmgrlem  27753  3vfriswmgr  27754  1to2vfriswmgr  27755  3cyclfrgrrn1  27761  4cycl2vnunb  27766  n4cyclfrgr  27767  vdgn1frgrv2  27772  frgrncvvdeqlem3  27777  frgrncvvdeqlem8  27782  frgrwopregbsn  27793  frgrwopreglem5ALT  27798  fusgr2wsp2nb  27810  esumpr2  30948  cplgredgex  31984  altopthsn  33037  dihprrn  38118  dvh3dim  38138  mapdindp2  38413  elsprel  43145  prelspr  43156  sprsymrelfolem2  43163  reupr  43192  reuopreuprim  43196  isomuspgrlem2d  43504  upgrwlkupwlk  43523  inlinecirc02plem  44280