Theorem breq12 5154

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150

This theorem is referenced by:  breq12i  5158  breq12d  5162  breqan12d  5165  rbropapd  5566  posn  5763  dfrel4  6197  dfpo2  6302  isopolem  7352  poxp  8133  soxp  8134  fnse  8138  poxp2  8148  poxp3  8155  ecopover  8840  canth2g  9159  ttrclss  9750  ttrclselem2  9756  infxpen  10044  sornom  10307  dcomex  10477  zorn2lem6  10531  brdom6disj  10562  fpwwe2  10673  rankcf  10807  ltresr  11170  ltxrlt  11321  wloglei  11783  ltxr  13135  xrltnr  13139  xrltnsym  13156  xrlttri  13158  xrlttr  13159  brfi1uzind  14500  brfi1indALT  14502  f1olecpbl  17517  isfull  17907  isfth  17911  prslem  18298  pslem  18572  dirtr  18602  xrsdsval  21365  dvcvx  26002  2sqmo  27420  2sqreultblem  27431  2sqreunnltblem  27434  2sqreuopb  27451  ssltsn  27776  slerec  27803  addsproplem2  27938  negsproplem2  27992  recut  28301  0reno  28302  axcontlem9  28860  isrusgr  29452  wlk2f  29521  istrlson  29598  upgrwlkdvspth  29630  ispthson  29633  isspthson  29634  crctcshwlk  29710  crctcsh  29712  2pthon3v  29831  umgr2wlk  29837  0pthonv  30016  1pthon2v  30040  uhgr3cyclex  30069  brfinext  33478  mclsppslem  35326  fununiq  35497  elfix2  35633  poimirlem10  37236  poimirlem11  37237  factwoffsmonot  41830  dvdsexpnn0  42038  monotoddzzfi  42507  or2expropbi  46556  dfatcolem  46775  sprsymrelfolem2  46972  poprelb  47003  lindepsnlininds  47708  catprslem  48204