Theorem breq12 5108

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

Assertion

Ref	Expression
breq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breq12

Step	Hyp	Ref	Expression
1		breq1 5106	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2		breq2 5107	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷))
3	1, 2	sylan9bb 519	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breq12i  5112  breq12d  5116  breqan12d  5119  rbropapd  5541  posn  5741  dfrel4  6186  dfpo2  6296  isopolem  7349  poxp  8131  soxp  8132  fnse  8136  poxp2  8146  poxp3  8153  ecopover  8828  canth2g  9136  ttrclss  9706  ttrclselem2  9712  infxpen  10042  sornom  10304  dcomex  10474  zorn2lem6  10528  brdom6disj  10560  fpwwe2  10677  rankcf  10811  ltresr  11174  ltxrlt  11329  wloglei  11795  ltxr  13191  xrltnr  13195  xrltnsym  13213  xrlttri  13215  xrlttr  13216  brfi1uzind  14598  brfi1indALT  14600  f1olecpbl  17638  isfull  18026  isfth  18030  prslem  18410  pslem  18685  dirtr  18715  xrsdsval  21656  dvcvx  26279  2sqmo  27705  2sqreultblem  27716  2sqreunnltblem  27719  2sqreuopb  27736  lesrec  28096  addsproplem2  28267  negsproplem2  28326  recut  28791  elreno2  28792  axcontlem9  29461  isrusgr  30053  wlk2f  30121  istrlson  30200  upgrwlkdvspth  30236  ispthson  30239  isspthson  30240  crctcshwlk  30322  crctcsh  30324  2pthon3v  30443  umgr2wlk  30449  0pthonv  30631  1pthon2v  30665  uhgr3cyclex  30694  brfinext  34195  finextfldext  34207  bralgext  34240  mclsppslem  36245  fununiq  36431  elfix2  36564  poimirlem10  38444  poimirlem11  38445  dvdsexpnn0  43274  monotoddzzfi  43848  or2expropbi  47987  dfatcolem  48208  sprsymrelfolem2  48458  poprelb  48489  cycldlenngric  48909  gpgprismgr4cyclex  49088  lgricngricex  49110  lindepsnlininds  49447  catprslem  50001