Theorem breq12 5079

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  breq12i  5083  breq12d  5087  breqan12d  5090  rbropapd  5477  posn  5672  dfrel4  6094  dfpo2  6199  isopolem  7216  poxp  7969  soxp  7970  fnse  7974  ecopover  8610  canth2g  8918  ttrclss  9478  ttrclselem2  9484  infxpen  9770  sornom  10033  dcomex  10203  zorn2lem6  10257  brdom6disj  10288  fpwwe2  10399  rankcf  10533  ltresr  10896  ltxrlt  11045  wloglei  11507  ltxr  12851  xrltnr  12855  xrltnsym  12871  xrlttri  12873  xrlttr  12874  brfi1uzind  14212  brfi1indALT  14214  f1olecpbl  17238  isfull  17626  isfth  17630  prslem  18016  pslem  18290  dirtr  18320  xrsdsval  20642  dvcvx  25184  2sqmo  26585  2sqreultblem  26596  2sqreunnltblem  26599  2sqreuopb  26616  axcontlem9  27340  isrusgr  27928  wlk2f  27997  istrlson  28075  upgrwlkdvspth  28107  ispthson  28110  isspthson  28111  crctcshwlk  28187  crctcsh  28189  2pthon3v  28308  umgr2wlk  28314  0pthonv  28493  1pthon2v  28517  uhgr3cyclex  28546  brfinext  31728  mclsppslem  33545  fununiq  33743  poxp2  33790  poxp3  33796  slerec  34013  elfix2  34206  poimirlem10  35787  poimirlem11  35788  factwoffsmonot  40163  dvdsexpnn0  40341  monotoddzzfi  40764  or2expropbi  44528  dfatcolem  44747  sprsymrelfolem2  44945  poprelb  44976  lindepsnlininds  45793  catprslem  46291