Theorem breq12 5148

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  breq12i  5152  breq12d  5156  breqan12d  5159  rbropapd  5569  posn  5771  dfrel4  6211  dfpo2  6316  isopolem  7365  poxp  8153  soxp  8154  fnse  8158  poxp2  8168  poxp3  8175  ecopover  8861  canth2g  9171  ttrclss  9760  ttrclselem2  9766  infxpen  10054  sornom  10317  dcomex  10487  zorn2lem6  10541  brdom6disj  10572  fpwwe2  10683  rankcf  10817  ltresr  11180  ltxrlt  11331  wloglei  11795  ltxr  13157  xrltnr  13161  xrltnsym  13179  xrlttri  13181  xrlttr  13182  brfi1uzind  14547  brfi1indALT  14549  f1olecpbl  17572  isfull  17957  isfth  17961  prslem  18343  pslem  18617  dirtr  18647  xrsdsval  21428  dvcvx  26059  2sqmo  27481  2sqreultblem  27492  2sqreunnltblem  27495  2sqreuopb  27512  ssltsn  27837  slerec  27864  addsproplem2  28003  negsproplem2  28061  nohalf  28407  recut  28428  0reno  28429  axcontlem9  28987  isrusgr  29579  wlk2f  29648  istrlson  29725  upgrwlkdvspth  29759  ispthson  29762  isspthson  29763  crctcshwlk  29842  crctcsh  29844  2pthon3v  29963  umgr2wlk  29969  0pthonv  30148  1pthon2v  30172  uhgr3cyclex  30201  brfinext  33704  mclsppslem  35588  fununiq  35769  elfix2  35905  poimirlem10  37637  poimirlem11  37638  factwoffsmonot  42243  dvdsexpnn0  42369  monotoddzzfi  42954  or2expropbi  47046  dfatcolem  47267  sprsymrelfolem2  47480  poprelb  47511  lindepsnlininds  48369  catprslem  48899