Theorem preq2 4269

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

Syntax hints:   → wi 4   = wceq 1483  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  preq12  4270  preq2i  4272  preq2d  4275  tpeq2  4278  ifpprsnss  4299  preq12bg  4386  prel12g  4387  elpreqprlem  4395  elpr2elpr  4398  opeq2  4403  uniprg  4450  intprg  4511  prex  4909  opth  4945  opeqsn  4967  propeqop  4970  relop  5272  funopg  5922  f1oprswap  6180  fprg  6422  fnprb  6472  fnpr2g  6474  pr2ne  8828  prdom2  8829  dfac2  8953  brdom7disj  9353  brdom6disj  9354  wunpr  9531  wunex2  9560  wuncval2  9569  grupr  9619  prunioo  12301  hashprg  13182  hashprgOLD  13183  wwlktovf  13699  wwlktovfo  13701  wrd2f1tovbij  13703  joindef  17004  meetdef  17018  lspfixed  19128  hmphindis  21600  upgrex  25987  edglnl  26038  usgredg4  26109  usgredgreu  26110  uspgredg2vtxeu  26112  uspgredg2v  26116  nbgrel  26238  nbupgrel  26241  nbumgrvtx  26242  nbusgreledg  26249  nbgrnself  26257  nb3grprlem1  26282  nb3grprlem2  26283  uvtxael1  26296  uvtxusgrel  26304  cusgredg  26320  usgredgsscusgredg  26355  1egrvtxdg0  26407  ifpsnprss  26518  upgriswlk  26537  uspgrn2crct  26700  wwlksnextfun  26793  wwlksnextsur  26795  wwlksnextbij  26797  clwlkclwwlklem2  26901  clwwlkinwwlk  26905  upgr1wlkdlem1  27005  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eupth2lem3lem4  27091  frcond1  27130  frgr1v  27135  nfrgr2v  27136  frgr3v  27139  1vwmgr  27140  3vfriswmgrlem  27141  3vfriswmgr  27142  1to2vfriswmgr  27143  3cyclfrgrrn1  27149  4cycl2vnunb  27154  n4cyclfrgr  27155  vdgn1frgrv2  27160  frgrncvvdeqlem3  27165  frgrncvvdeqlem8  27170  frgrwopregbsn  27181  frgrwopreglem5ALT  27186  fusgr2wsp2nb  27198  numclwwlkovf2ex  27219  esumpr2  30129  altopthsn  32068  dihprrn  36715  dvh3dim  36735  mapdindp2  37010  upgrwlkupwlk  41721  elsprel  41725  prelspr  41736  sprsymrelfolem2  41743