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

Theorem preq1d 4217
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypothesis
Ref Expression
preq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
preq1d (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})

Proof of Theorem preq1d
StepHypRef Expression
1 preq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 preq1 4211 . 2 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
31, 2syl 17 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:  opthwiener  4892  fprg  6305  fnpr2g  6357  dfac2  8813  symg2bas  17587  2pthoncl  25899  wwlknredwwlkn  26020  wwlkextprop  26038  clwwlkgt0  26065  clwlkisclwwlklem2fv1  26076  clwlkisclwwlklem2fv2  26077  clwlkisclwwlklem2a  26079  clwlkisclwwlklem0  26082  clwwisshclwwlem  26100  eupath2lem3  26272  frgraunss  26288  frgra1v  26291  frgra2v  26292  frgra3v  26295  n4cyclfrgra  26311  fprb  30722  wopprc  36418  propeqop  40126  crctcsh1wlkn0lem6  41020  wwlksnredwwlkn  41103  wwlksnextprop  41120  clwlkclwwlklem2fv1  41206  clwlkclwwlklem2fv2  41207  clwlkclwwlklem2a  41209  clwlkclwwlklem3  41212  clwwlks1loop  41217  clwwlksn1loop  41218  clwwisshclwwslem  41236  frcond1  41440  frgr1v  41443  nfrgr2v  41444  frgr3v  41447  n4cyclfrgr  41463
  Copyright terms: Public domain W3C validator