Theorem breq12 5124

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  breq12i  5128  breq12d  5132  breqan12d  5135  rbropapd  5539  posn  5740  dfrel4  6180  dfpo2  6285  isopolem  7338  poxp  8127  soxp  8128  fnse  8132  poxp2  8142  poxp3  8149  ecopover  8835  canth2g  9145  ttrclss  9734  ttrclselem2  9740  infxpen  10028  sornom  10291  dcomex  10461  zorn2lem6  10515  brdom6disj  10546  fpwwe2  10657  rankcf  10791  ltresr  11154  ltxrlt  11305  wloglei  11769  ltxr  13131  xrltnr  13135  xrltnsym  13153  xrlttri  13155  xrlttr  13156  brfi1uzind  14526  brfi1indALT  14528  f1olecpbl  17541  isfull  17925  isfth  17929  prslem  18309  pslem  18582  dirtr  18612  xrsdsval  21378  dvcvx  25977  2sqmo  27400  2sqreultblem  27411  2sqreunnltblem  27414  2sqreuopb  27431  ssltsn  27756  slerec  27783  addsproplem2  27929  negsproplem2  27987  recut  28399  0reno  28400  axcontlem9  28951  isrusgr  29541  wlk2f  29610  istrlson  29687  upgrwlkdvspth  29721  ispthson  29724  isspthson  29725  crctcshwlk  29804  crctcsh  29806  2pthon3v  29925  umgr2wlk  29931  0pthonv  30110  1pthon2v  30134  uhgr3cyclex  30163  brfinext  33694  mclsppslem  35605  fununiq  35786  elfix2  35922  poimirlem10  37654  poimirlem11  37655  factwoffsmonot  42255  dvdsexpnn0  42383  monotoddzzfi  42966  or2expropbi  47063  dfatcolem  47284  sprsymrelfolem2  47507  poprelb  47538  cycldlenngric  47941  gpgprismgr4cyclex  48106  lindepsnlininds  48428  catprslem  48985