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

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

Proof of Theorem preq2
StepHypRef Expression
1 preq1 4259 . 2 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2 prcom 4258 . 2 {𝐶, 𝐴} = {𝐴, 𝐶}
3 prcom 4258 . 2 {𝐶, 𝐵} = {𝐵, 𝐶}
41, 2, 33eqtr4g 2679 1 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1481  {cpr 4170 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-sn 4169  df-pr 4171 This theorem is referenced by:  preq12  4261  preq2i  4263  preq2d  4266  tpeq2  4269  ifpprsnss  4290  preq12bg  4377  prel12g  4378  elpreqprlem  4386  elpr2elpr  4389  opeq2  4394  uniprg  4441  intprg  4502  prex  4900  opth  4935  opeqsn  4957  propeqop  4960  relop  5261  funopg  5910  f1oprswap  6167  fprg  6407  fnprb  6457  fnpr2g  6459  pr2ne  8813  prdom2  8814  dfac2  8938  brdom7disj  9338  brdom6disj  9339  wunpr  9516  wunex2  9545  wuncval2  9554  grupr  9604  prunioo  12286  hashprg  13165  hashprgOLD  13166  wwlktovf  13680  wwlktovfo  13682  wrd2f1tovbij  13684  isprm2lem  15375  joindef  16985  meetdef  16999  lspfixed  19109  hmphindis  21581  upgrex  25968  edglnl  26019  usgredg4  26090  usgredgreu  26091  uspgredg2vtxeu  26093  uspgredg2v  26097  nbgrel  26219  nbupgrel  26222  nbumgrvtx  26223  nbusgreledg  26230  nbgrnself  26238  nb3grprlem1  26263  nb3grprlem2  26264  uvtxael1  26277  uvtxusgrel  26285  cusgredg  26301  usgredgsscusgredg  26336  1egrvtxdg0  26388  ifpsnprss  26499  upgriswlk  26518  uspgrn2crct  26681  wwlksnextfun  26774  wwlksnextsur  26776  wwlksnextbij  26778  clwlkclwwlklem2  26882  upgr1wlkdlem1  26985  upgr3v3e3cycl  27020  upgr4cycl4dv4e  27025  eupth2lem3lem4  27071  frcond1  27110  frgr1v  27115  nfrgr2v  27116  frgr3v  27119  1vwmgr  27120  3vfriswmgrlem  27121  3vfriswmgr  27122  1to2vfriswmgr  27123  3cyclfrgrrn1  27129  4cycl2vnunb  27134  n4cyclfrgr  27135  vdgn1frgrv2  27140  frgrncvvdeqlem3  27145  frgrncvvdeqlem8  27150  frgrwopreg2  27161  fusgr2wsp2nb  27172  extwwlkfablem1  27182  numclwwlkovf2ex  27191  esumpr2  30103  altopthsn  32043  dihprrn  36534  dvh3dim  36554  mapdindp2  36829  upgrwlkupwlk  41486  elsprel  41490  prelspr  41501  sprsymrelfolem2  41508
 Copyright terms: Public domain W3C validator