Theorem breq12 5101

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

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

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  breq12i  5105  breq12d  5109  breqan12d  5112  rbropapd  5508  posn  5708  dfrel4  6147  dfpo2  6252  isopolem  7289  poxp  8068  soxp  8069  fnse  8073  poxp2  8083  poxp3  8090  ecopover  8756  canth2g  9057  ttrclss  9627  ttrclselem2  9633  infxpen  9922  sornom  10185  dcomex  10355  zorn2lem6  10409  brdom6disj  10440  fpwwe2  10552  rankcf  10686  ltresr  11049  ltxrlt  11201  wloglei  11667  ltxr  13027  xrltnr  13031  xrltnsym  13049  xrlttri  13051  xrlttr  13052  brfi1uzind  14429  brfi1indALT  14431  f1olecpbl  17446  isfull  17834  isfth  17838  prslem  18218  pslem  18493  dirtr  18523  xrsdsval  21363  dvcvx  25979  2sqmo  27402  2sqreultblem  27413  2sqreunnltblem  27416  2sqreuopb  27433  slerec  27787  addsproplem2  27940  negsproplem2  27998  recut  28439  elreno2  28440  axcontlem9  28994  isrusgr  29584  wlk2f  29652  istrlson  29727  upgrwlkdvspth  29761  ispthson  29764  isspthson  29765  crctcshwlk  29844  crctcsh  29846  2pthon3v  29965  umgr2wlk  29971  0pthonv  30153  1pthon2v  30177  uhgr3cyclex  30206  brfinext  33758  finextfldext  33770  bralgext  33803  mclsppslem  35726  fununiq  35912  elfix2  36045  poimirlem10  37770  poimirlem11  37771  dvdsexpnn0  42531  monotoddzzfi  43126  or2expropbi  47222  dfatcolem  47443  sprsymrelfolem2  47681  poprelb  47712  cycldlenngric  48116  gpgprismgr4cyclex  48295  lgricngricex  48317  lindepsnlininds  48640  catprslem  49197