Theorem breq12 5152

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  breq12i  5156  breq12d  5160  breqan12d  5163  rbropapd  5573  posn  5773  dfrel4  6212  dfpo2  6317  isopolem  7364  poxp  8151  soxp  8152  fnse  8156  poxp2  8166  poxp3  8173  ecopover  8859  canth2g  9169  ttrclss  9757  ttrclselem2  9763  infxpen  10051  sornom  10314  dcomex  10484  zorn2lem6  10538  brdom6disj  10569  fpwwe2  10680  rankcf  10814  ltresr  11177  ltxrlt  11328  wloglei  11792  ltxr  13154  xrltnr  13158  xrltnsym  13175  xrlttri  13177  xrlttr  13178  brfi1uzind  14543  brfi1indALT  14545  f1olecpbl  17573  isfull  17963  isfth  17967  prslem  18354  pslem  18629  dirtr  18659  xrsdsval  21445  dvcvx  26073  2sqmo  27495  2sqreultblem  27506  2sqreunnltblem  27509  2sqreuopb  27526  ssltsn  27851  slerec  27878  addsproplem2  28017  negsproplem2  28075  nohalf  28421  recut  28442  0reno  28443  axcontlem9  29001  isrusgr  29593  wlk2f  29662  istrlson  29739  upgrwlkdvspth  29771  ispthson  29774  isspthson  29775  crctcshwlk  29851  crctcsh  29853  2pthon3v  29972  umgr2wlk  29978  0pthonv  30157  1pthon2v  30181  uhgr3cyclex  30210  brfinext  33680  fldext2chn  33733  mclsppslem  35567  fununiq  35749  elfix2  35885  poimirlem10  37616  poimirlem11  37617  factwoffsmonot  42223  dvdsexpnn0  42347  monotoddzzfi  42930  or2expropbi  46983  dfatcolem  47204  sprsymrelfolem2  47417  poprelb  47448  lindepsnlininds  48297  catprslem  48798