Theorem breqan12d 4467

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypotheses

Ref	Expression
breq1d.1
breqan12i.2

Assertion

Ref	Expression
breqan12d

Proof of Theorem breqan12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2
2		breqan12i.2	. 2
3		breq12 4457	. 2
4	1, 2, 3	syl2an 477	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395   class class class wbr 4452

This theorem is referenced by:  breqan12rd  4468  soisores  6223  isoid  6225  isores3  6231  isoini2  6235  ofrfval  6548  fnwelem  6915  fnse  6917  wemaplem1  7992  r0weon  8411  sornom  8678  enqbreq2  9319  nqereu  9328  ordpinq  9342  lterpq  9369  ltresr2  9539  axpre-ltadd  9565  leltadd  10061  lemul1a  10421  negiso  10544  xltneg  11445  lt2sq  12241  le2sq  12242  sqrtle  13094  prdsleval  14874  efgcpbllema  16772  iducn  20786  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  reefiso  22843  sinord  22921  logltb  22984  logccv  23044  atanord  23258  birthdaylem3  23283  lgsquadlem3  23631  mddmd  27220  xrge0iifiso  27917  erdszelem4  28638  erdszelem8  28642  cgrextend  29658  monotuz  30877  monotoddzzfi  30878  expmordi  30883  wepwsolem  30987  fnwe2val  30995  aomclem8  31007  idlaut  35820

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-3an 975  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-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453