Theorem preq12d 4740

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

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		preq12 4734	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Syntax hints:   → wi 4   = wceq 1539  {cpr 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-sn 4626  df-pr 4628

This theorem is referenced by:  opeq1  4872  csbopg  4890  opthhausdorff  5521  opthhausdorff0  5522  f1oprswap  6891  wunex2  10779  wuncval2  10788  s4prop  14950  wrdlen2  14984  wwlktovf  14996  wwlktovf1  14997  wwlktovfo  14998  wrd2f1tovbij  15000  prdsval  17501  xpsfval  17612  xpsval  17616  ipoval  18576  frmdval  18865  symg2bas  19411  xpstopnlem2  23820  tusval  24275  tmsval  24494  tmsxpsval  24552  uniiccdif  25614  dchrval  27279  eengv  28995  wkslem1  29626  wkslem2  29627  iswlk  29629  wlkonl1iedg  29684  2wlklem  29686  redwlk  29691  wlkp1lem7  29698  wlkdlem2  29702  upgrwlkdvdelem  29757  usgr2pthlem  29784  usgr2pth  29785  crctcshwlkn0lem4  29834  crctcshwlkn0lem5  29835  crctcshwlkn0lem6  29836  iswwlks  29857  0enwwlksnge1  29885  wlkiswwlks2lem2  29891  wlkiswwlks2lem5  29894  wwlksm1edg  29902  wwlksnred  29913  wwlksnext  29914  wwlksnredwwlkn  29916  wwlksnextproplem2  29931  2wlkdlem10  29956  umgrwwlks2on  29978  rusgrnumwwlkl1  29989  isclwwlk  30004  clwwlkccatlem  30009  clwwlkccat  30010  clwlkclwwlklem2a1  30012  clwlkclwwlklem2fv1  30015  clwlkclwwlklem2a4  30017  clwlkclwwlklem2a  30018  clwlkclwwlklem2  30020  clwlkclwwlk  30022  clwwisshclwwslemlem  30033  clwwisshclwwslem  30034  clwwisshclwws  30035  clwwlkinwwlk  30060  clwwlkn2  30064  clwwlkel  30066  clwwlkf  30067  clwwlkwwlksb  30074  clwwlkext2edg  30076  wwlksext2clwwlk  30077  wwlksubclwwlk  30078  umgr2cwwk2dif  30084  s2elclwwlknon2  30124  clwwlknonex2lem2  30128  clwwlknonex2  30129  3wlkdlem10  30189  upgr3v3e3cycl  30200  upgr4cycl4dv4e  30205  eupthseg  30226  upgreupthseg  30229  eupth2lem3  30256  nfrgr2v  30292  frgr3vlem1  30293  frgr3vlem2  30294  4cycl2vnunb  30310  disjdifprg  32589  s2rnOLD  32929  idlsrgval  33532  revwlk  35131  kur14lem1  35212  kur14  35222  bj-endval  37317  tgrpfset  40747  tgrpset  40748  hlhilset  41937  dfac21  43083  mendval  43196  oaun2  43399  mnurndlem1  44305  sge0sn  46399  isuspgrimlem  47879  grtriproplem  47911  isgrtri  47915  grtriclwlk3  47917  cycl3grtrilem  47918  stgrfv  47925  gpgov  48006  gpgedgvtx0  48024  gpgedgvtx1  48025  gpg3kgrtriexlem6  48049  gpg3kgrtriex  48050  isupwlk  48057  zlmodzxzsub  48281  2arymaptf  48578  prelrrx2b  48640  rrx2plordisom  48649  onsetreclem1  49279