Theorem preq12d 4220

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 4214	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
4	1, 2, 3	syl2anc 691	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Syntax hints:   → wi 4   = wceq 1475  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  opeq1  4340  csbopg  4358  f1oprswap  6092  wunex2  9439  wuncval2  9448  s4prop  13505  wrdlen2  13536  wwlktovf  13547  wwlktovf1  13548  wwlktovfo  13549  wrd2f1tovbij  13551  prdsval  15938  ipoval  16977  frmdval  17211  symg2bas  17641  tusval  21880  tmsval  22096  tmsxpsval  22153  uniiccdif  23152  dchrval  24759  eengv  25659  iswlk  26048  wlkelwrd  26058  istrl  26067  wlkntrllem2  26090  2wlklem  26094  constr1trl  26118  2pthlem2  26126  2wlklem1  26127  redwlk  26136  wlkdvspthlem  26137  3v3e3cycl1  26172  constr3trllem5  26182  4cycl4v4e  26194  4cycl4dv4e  26196  iswwlk  26211  wlkiswwlk2lem2  26220  wlkiswwlk2lem5  26223  wwlknred  26251  wwlknext  26252  wwlknredwwlkn  26254  wwlkm1edg  26263  wwlkextproplem2  26270  isclwwlk  26296  clwwlkprop  26298  clwwlkgt0  26299  clwwlkn2  26303  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlk  26317  clwwlkel  26321  clwwlkf  26322  clwwlkext2edg  26330  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwwisshclwwlem1  26333  clwwisshclwwlem  26334  clwwisshclww  26335  usg2cwwk2dif  26348  clwlkfclwwlk  26371  rusgrasn  26472  rusgranumwlkl1  26474  iseupa  26492  eupatrl  26495  eupaseg  26500  eupares  26502  eupap1  26503  eupath2lem3  26506  frgra2v  26526  frgra3vlem1  26527  frgra3vlem2  26528  4cycl2vnunb  26544  extwwlkfablem1  26601  extwwlkfablem2  26605  numclwwlkovf2ex  26613  disjdifprg  28770  kur14lem1  30442  kur14  30452  tgrpfset  35050  tgrpset  35051  hlhilset  36244  dfac21  36654  mendval  36772  sge0sn  39272  1wlkslem1  40809  1wlkslem2  40810  is1wlk  40813  isWlk  40814  wlkOnl1iedg  40873  2Wlklem  40875  red1wlk  40881  1wlkp1lem7  40888  1wlkp1lem8  40889  1wlkdlem2  40892  upgrwlkdvdelem  40942  usgr2wlkneq  40962  usgr2trlncl  40966  usgr2pthlem  40969  usgr2pth  40970  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  iswwlks  41039  0enwwlksnge1  41060  1wlkiswwlks2lem2  41067  1wlkiswwlks2lem5  41070  wwlksm1edg  41078  wwlksnred  41098  wwlksnext  41099  wwlksnredwwlkn  41101  wwlksnextproplem2  41116  21wlkdlem10  41142  umgrwwlks2on  41161  rusgrnumwwlkl1  41172  isclwwlks  41188  clwlkclwwlklem2a1  41201  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlk  41211  clwwlksn2  41217  clwwlksel  41221  clwwlksf  41222  clwwlksext2edg  41230  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwwisshclwwslemlem  41233  clwwisshclwwslem  41234  clwwisshclwws  41235  umgr2cwwk2dif  41248  clwlksfclwwlk  41269  31wlkdlem10  41336  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupthseg  41374  upgreupthseg  41377  eupth2lem3  41404  nfrgr2v  41442  frgr3vlem1  41443  frgr3vlem2  41444  4cycl2vnunb-av  41460  av-extwwlkfablem1  41508  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  zlmodzxzsub  41931  onsetreclem1  42247