Theorem breq12 5153

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 5151	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2		breq2 5152	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷))
3	1, 2	sylan9bb 510	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breq12i  5157  breq12d  5161  breqan12d  5164  rbropapd  5564  posn  5761  dfrel4  6190  dfpo2  6295  isopolem  7341  poxp  8113  soxp  8114  fnse  8118  poxp2  8128  poxp3  8135  ecopover  8814  canth2g  9130  ttrclss  9714  ttrclselem2  9720  infxpen  10008  sornom  10271  dcomex  10441  zorn2lem6  10495  brdom6disj  10526  fpwwe2  10637  rankcf  10771  ltresr  11134  ltxrlt  11283  wloglei  11745  ltxr  13094  xrltnr  13098  xrltnsym  13115  xrlttri  13117  xrlttr  13118  brfi1uzind  14458  brfi1indALT  14460  f1olecpbl  17472  isfull  17860  isfth  17864  prslem  18250  pslem  18524  dirtr  18554  xrsdsval  20988  dvcvx  25536  2sqmo  26937  2sqreultblem  26948  2sqreunnltblem  26951  2sqreuopb  26968  slerec  27317  addsproplem2  27451  negsproplem2  27500  axcontlem9  28227  isrusgr  28815  wlk2f  28884  istrlson  28961  upgrwlkdvspth  28993  ispthson  28996  isspthson  28997  crctcshwlk  29073  crctcsh  29075  2pthon3v  29194  umgr2wlk  29200  0pthonv  29379  1pthon2v  29403  uhgr3cyclex  29432  brfinext  32727  mclsppslem  34569  fununiq  34735  elfix2  34871  poimirlem10  36493  poimirlem11  36494  factwoffsmonot  41018  dvdsexpnn0  41232  monotoddzzfi  41671  or2expropbi  45734  dfatcolem  45953  sprsymrelfolem2  46151  poprelb  46182  lindepsnlininds  47123  catprslem  47620