Theorem breq12 5075

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  breq12i  5079  breq12d  5083  breqan12d  5086  rbropapd  5468  posn  5663  dfrel4  6083  dfpo2  6188  isopolem  7196  poxp  7940  soxp  7941  fnse  7945  ecopover  8568  canth2g  8867  infxpen  9701  sornom  9964  dcomex  10134  zorn2lem6  10188  brdom6disj  10219  fpwwe2  10330  rankcf  10464  ltresr  10827  ltxrlt  10976  wloglei  11437  ltxr  12780  xrltnr  12784  xrltnsym  12800  xrlttri  12802  xrlttr  12803  brfi1uzind  14140  brfi1indALT  14142  f1olecpbl  17155  isfull  17542  isfth  17546  prslem  17931  pslem  18205  dirtr  18235  xrsdsval  20554  dvcvx  25089  2sqmo  26490  2sqreultblem  26501  2sqreunnltblem  26504  2sqreuopb  26521  axcontlem9  27243  isrusgr  27831  wlk2f  27899  istrlson  27976  upgrwlkdvspth  28008  ispthson  28011  isspthson  28012  crctcshwlk  28088  crctcsh  28090  2pthon3v  28209  umgr2wlk  28215  0pthonv  28394  1pthon2v  28418  uhgr3cyclex  28447  brfinext  31630  mclsppslem  33445  fununiq  33649  ttrclss  33706  ttrclselem2  33712  poxp2  33717  poxp3  33723  slerec  33940  elfix2  34133  poimirlem10  35714  poimirlem11  35715  factwoffsmonot  40091  dvdsexpnn0  40262  monotoddzzfi  40680  or2expropbi  44415  dfatcolem  44634  sprsymrelfolem2  44833  poprelb  44864  lindepsnlininds  45681  catprslem  46179