MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  preq2 Structured version   Visualization version   GIF version

Theorem preq2 4212
Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
preq2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2
StepHypRef Expression
1 preq1 4211 . 2 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2 prcom 4210 . 2 {𝐶, 𝐴} = {𝐴, 𝐶}
3 prcom 4210 . 2 {𝐶, 𝐵} = {𝐵, 𝐶}
41, 2, 33eqtr4g 2668 1 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-sn 4125  df-pr 4127
This theorem is referenced by:  preq12  4213  preq2i  4215  preq2d  4218  tpeq2  4221  preq12bg  4321  prel12g  4322  elpreqprlem  4328  opeq2  4335  uniprg  4380  intprg  4440  prex  4831  opth  4865  opeqsn  4886  relop  5182  funopg  5822  f1oprswap  6077  fprg  6305  fnprb  6355  fnpr2g  6357  pr2ne  8688  prdom2  8689  dfac2  8813  brdom7disj  9211  brdom6disj  9212  wunpr  9387  wunex2  9416  wuncval2  9425  grupr  9475  prunioo  12128  hashprg  12995  hashprgOLD  12996  wwlktovf  13493  wwlktovfo  13495  wrd2f1tovbij  13497  isprm2lem  15178  joindef  16773  meetdef  16787  lspfixed  18895  hmphindis  21352  umgraex  25618  usgraedg4  25682  usgraedgreu  25683  nbgrael  25721  nbgraeledg  25725  nbgranself  25729  nbgraf1olem4  25739  nb3graprlem1  25746  nb3graprlem2  25747  cusgrarn  25754  cusgra1v  25756  cusgra2v  25757  nbcusgra  25758  cusgra3v  25759  usgrasscusgra  25777  uvtxel  25783  uvtxnbgra  25787  cusgrauvtxb  25790  uvtxnb  25791  constr2pth  25897  usgra2wlkspthlem1  25913  3v3e3cycl1  25938  constr3pthlem3  25951  4cycl4v4e  25960  4cycl4dv  25961  4cycl4dv4e  25962  wwlkextfun  26023  wwlkextsur  26025  wwlkextbij  26027  clwlkisclwwlklem1  26081  usg2spthonot0  26182  frgraunss  26288  frgra1v  26291  frgra2v  26292  frgra3v  26295  1vwmgra  26296  3vfriswmgralem  26297  3vfriswmgra  26298  1to2vfriswmgra  26299  3cyclfrgrarn1  26305  4cycl2vnunb  26310  n4cyclfrgra  26311  vdn0frgrav2  26316  vdgn0frgrav2  26317  vdn1frgrav2  26318  vdgn1frgrav2  26319  frgrancvvdeqlem4  26326  frgrancvvdeqlemB  26331  frgrawopreglem5  26341  frgrawopreg2  26344  frg2woteqm  26352  usg2spot2nb  26358  numclwwlkovf2ex  26379  esumpr2  29262  altopthsn  31044  dihprrn  35536  dvh3dim  35556  mapdindp2  35831  propeqop  40126  elpr2elpr  40130  upgrex  40320  upgredg  40372  usgredg4  40446  usgredgreu  40447  uspgredg2vtxeu  40449  uspgredg2v  40453  nbgrel  40566  nbupgrel  40569  nbumgrvtx  40570  nbusgreledg  40577  nbgrnself  40585  nb3grprlem1  40610  nb3grprlem2  40611  uvtxael1  40624  uvtxusgrel  40632  cusgredg  40648  usgredgsscusgredg  40677  1egrvtxdg0  40729  1wlkvtxeledglem  40829  ifpprsnss  40847  upgr1wlkwlk  40849  uspgrn2crct  41013  wwlksnextfun  41106  wwlksnextsur  41108  wwlksnextbij  41110  clwlkclwwlklem2  41211  upgr11wlkdlem1  41314  upgr3v3e3cycl  41349  upgr4cycl4dv4e  41354  eupth2lem3lem4  41401  frcond1  41440  frgr1v  41443  nfrgr2v  41444  frgr3v  41447  1vwmgr  41448  3vfriswmgrlem  41449  3vfriswmgr  41450  1to2vfriswmgr  41451  3cyclfrgrrn1  41457  4cycl2vnunb-av  41462  n4cyclfrgr  41463  vdgn1frgrv2  41468  frgrncvvdeqlem4  41474  frgrncvvdeqlemB  41479  frgrwopreglem5  41487  frgrwopreg2  41490  frgr2wwlkeqm  41498  fusgr2wsp2nb  41500  av-extwwlkfablem1  41510  av-numclwwlkovf2ex  41519
  Copyright terms: Public domain W3C validator