Theorem breq12 5100

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  breq12i  5104  breq12d  5108  breqan12d  5111  rbropapd  5507  posn  5707  dfrel4  6146  dfpo2  6251  isopolem  7288  poxp  8067  soxp  8068  fnse  8072  poxp2  8082  poxp3  8089  ecopover  8754  canth2g  9054  ttrclss  9620  ttrclselem2  9626  infxpen  9915  sornom  10178  dcomex  10348  zorn2lem6  10402  brdom6disj  10433  fpwwe2  10544  rankcf  10678  ltresr  11041  ltxrlt  11193  wloglei  11659  ltxr  13024  xrltnr  13028  xrltnsym  13046  xrlttri  13048  xrlttr  13049  brfi1uzind  14425  brfi1indALT  14427  f1olecpbl  17441  isfull  17829  isfth  17833  prslem  18213  pslem  18488  dirtr  18518  xrsdsval  21357  dvcvx  25962  2sqmo  27385  2sqreultblem  27396  2sqreunnltblem  27399  2sqreuopb  27416  slerec  27770  addsproplem2  27923  negsproplem2  27981  recut  28408  0reno  28409  axcontlem9  28961  isrusgr  29551  wlk2f  29619  istrlson  29694  upgrwlkdvspth  29728  ispthson  29731  isspthson  29732  crctcshwlk  29811  crctcsh  29813  2pthon3v  29932  umgr2wlk  29938  0pthonv  30120  1pthon2v  30144  uhgr3cyclex  30173  brfinext  33676  finextfldext  33688  bralgext  33721  mclsppslem  35638  fununiq  35824  elfix2  35957  poimirlem10  37680  poimirlem11  37681  dvdsexpnn0  42442  monotoddzzfi  43049  or2expropbi  47148  dfatcolem  47369  sprsymrelfolem2  47607  poprelb  47638  cycldlenngric  48042  gpgprismgr4cyclex  48221  lgricngricex  48243  lindepsnlininds  48567  catprslem  49125