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

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

Proof of Theorem preq12d
StepHypRef Expression
1 preq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 preq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 preq12 4415 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 696 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  {cpr 4324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-sn 4323  df-pr 4325
This theorem is referenced by:  opeq1  4554  csbopg  4572  opthhausdorff  5128  opthhausdorff0  5129  f1oprswap  6343  wunex2  9773  wuncval2  9782  s4prop  13876  wrdlen2  13910  wwlktovf  13921  wwlktovf1  13922  wwlktovfo  13923  wrd2f1tovbij  13925  prdsval  16338  ipoval  17376  frmdval  17610  symg2bas  18039  tusval  22292  tmsval  22508  tmsxpsval  22565  uniiccdif  23567  dchrval  25180  eengv  26080  wkslem1  26735  wkslem2  26736  iswlk  26738  wlkonl1iedg  26793  2wlklem  26795  redwlk  26801  wlkp1lem7  26808  wlkp1lem8  26809  wlkdlem2  26812  upgrwlkdvdelem  26864  usgr2pthlem  26891  usgr2pth  26892  crctcshwlkn0lem4  26938  crctcshwlkn0lem5  26939  crctcshwlkn0lem6  26940  iswwlks  26961  0enwwlksnge1  26995  wlkiswwlks2lem2  27001  wlkiswwlks2lem5  27004  wwlksm1edg  27012  wwlksnred  27032  wwlksnext  27033  wwlksnredwwlkn  27035  wwlksnextproplem2  27050  2wlkdlem10  27077  umgrwwlks2on  27100  rusgrnumwwlkl1  27112  isclwwlk  27129  clwwlkccatlem  27134  clwwlkccat  27135  clwlkclwwlklem2a1  27137  clwlkclwwlklem2fv1  27140  clwlkclwwlklem2a4  27142  clwlkclwwlklem2a  27143  clwlkclwwlklem2  27145  clwlkclwwlk  27147  clwwisshclwwslemlem  27158  clwwisshclwwslem  27159  clwwisshclwws  27160  clwwlkinwwlk  27191  clwwlkn2  27195  clwwlkel  27197  clwwlkf  27198  clwwlkwwlksb  27206  clwwlkext2edg  27208  wwlksext2clwwlk  27209  wwlksext2clwwlkOLD  27210  wwlksubclwwlk  27211  umgr2cwwk2dif  27217  clwlksfclwwlkOLD  27238  s2elclwwlknon2  27274  clwwlknonex2lem2  27279  clwwlknonex2  27280  3wlkdlem10  27343  upgr3v3e3cycl  27354  upgr4cycl4dv4e  27359  eupthseg  27380  upgreupthseg  27383  eupth2lem3  27410  nfrgr2v  27448  frgr3vlem1  27449  frgr3vlem2  27450  4cycl2vnunb  27466  extwwlkfablem1OLD  27519  disjdifprg  29717  kur14lem1  31517  kur14  31527  tgrpfset  36553  tgrpset  36554  hlhilset  37747  dfac21  38157  mendval  38274  sge0sn  41118  isupwlk  42246  zlmodzxzsub  42667  onsetreclem1  42980
  Copyright terms: Public domain W3C validator