Theorem breq12 5035

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  breq12i  5039  breq12d  5043  breqan12d  5046  rbropapd  5414  posn  5601  dfrel4  6015  isopolem  7077  poxp  7805  soxp  7806  fnse  7810  ecopover  8384  canth2g  8655  infxpen  9425  sornom  9688  dcomex  9858  zorn2lem6  9912  brdom6disj  9943  fpwwe2  10054  rankcf  10188  ltresr  10551  ltxrlt  10700  wloglei  11161  ltxr  12498  xrltnr  12502  xrltnsym  12518  xrlttri  12520  xrlttr  12521  brfi1uzind  13852  brfi1indALT  13854  f1olecpbl  16792  isfull  17172  isfth  17176  prslem  17533  pslem  17808  dirtr  17838  xrsdsval  20135  dvcvx  24623  2sqmo  26021  2sqreultblem  26032  2sqreunnltblem  26035  2sqreuopb  26052  axcontlem9  26766  isrusgr  27351  wlk2f  27419  istrlson  27496  upgrwlkdvspth  27528  ispthson  27531  isspthson  27532  crctcshwlk  27608  crctcsh  27610  2pthon3v  27729  umgr2wlk  27735  0pthonv  27914  1pthon2v  27938  uhgr3cyclex  27967  brfinext  31131  mclsppslem  32943  dfpo2  33104  fununiq  33125  slerec  33390  elfix2  33478  poimirlem10  35067  poimirlem11  35068  factwoffsmonot  39388  monotoddzzfi  39883  or2expropbi  43626  dfatcolem  43811  sprsymrelfolem2  44010  poprelb  44041  lindepsnlininds  44861