Theorem preq12d 4117

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 4111	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  =wceq 1395  {cpr 4031

This theorem is referenced by:  opeq1  4217  f1oprswap  5860  wunex2  9137  wuncval2  9146  s4prop  12863  wrdlen2  12886  wwlktovf  12894  wwlktovf1  12895  wwlktovfo  12896  wrd2f1tovbij  12898  prdsval  14852  ipoval  15784  frmdval  16019  symg2bas  16423  tusval  20769  tmsval  20984  tmsxpsval  21041  uniiccdif  21987  dchrval  23509  eengv  24282  iswlk  24520  wlkelwrd  24530  istrl  24539  wlkntrllem2  24562  2wlklem  24566  constr1trl  24590  2pthlem2  24598  2wlklem1  24599  redwlk  24608  wlkdvspthlem  24609  3v3e3cycl1  24644  constr3trllem5  24654  4cycl4v4e  24666  4cycl4dv4e  24668  iswwlk  24683  wlkiswwlk2lem2  24692  wlkiswwlk2lem5  24695  wwlknred  24723  wwlknext  24724  wwlknredwwlkn  24726  wwlkm1edg  24735  wwlkextproplem2  24742  isclwwlk  24768  clwwlkprop  24770  clwwlkgt0  24771  clwwlkn2  24775  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2fv1  24782  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwlkisclwwlk  24789  clwwlkel  24793  clwwlkf  24794  clwwlkext2edg  24802  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwwisshclwwlem1  24805  clwwisshclwwlem  24806  clwwisshclww  24807  usg2cwwk2dif  24820  clwlkfclwwlk  24844  rusgrasn  24945  rusgranumwlkl1  24947  iseupa  24965  eupatrl  24968  eupaseg  24973  eupares  24975  eupap1  24976  eupath2lem3  24979  frgra2v  24999  frgra3vlem1  25000  frgra3vlem2  25001  4cycl2vnunb  25017  extwwlkfablem1  25074  extwwlkfablem2  25078  numclwwlkovf2ex  25086  disjdifprg  27436  kur14lem1  28650  kur14  28660  dfac21  31012  mendval  31132  usgra2pthlem1  32353  usgra2pth  32354  usgra2adedglem1  32356  zlmodzxzsub  32949  tgrpfset  36470  tgrpset  36471  hlhilset  37664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032