Theorem breq12 5073

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   class class class wbr 5068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069

This theorem is referenced by:  breq12i  5077  breq12d  5081  breqan12d  5084  rbropapd  5451  posn  5639  dfrel4  6050  isopolem  7100  poxp  7824  soxp  7825  fnse  7829  ecopover  8403  canth2g  8673  infxpen  9442  sornom  9701  dcomex  9871  zorn2lem6  9925  brdom6disj  9956  fpwwe2  10067  rankcf  10201  ltresr  10564  ltxrlt  10713  wloglei  11174  ltxr  12513  xrltnr  12517  xrltnsym  12533  xrlttri  12535  xrlttr  12536  brfi1uzind  13859  brfi1indALT  13861  f1olecpbl  16802  isfull  17182  isfth  17186  prslem  17543  pslem  17818  dirtr  17848  xrsdsval  20591  dvcvx  24619  2sqmo  26015  2sqreultblem  26026  2sqreunnltblem  26029  2sqreuopb  26046  axcontlem9  26760  isrusgr  27345  wlk2f  27413  istrlson  27490  upgrwlkdvspth  27522  ispthson  27525  isspthson  27526  crctcshwlk  27602  crctcsh  27604  2pthon3v  27724  umgr2wlk  27730  0pthonv  27910  1pthon2v  27934  uhgr3cyclex  27963  brfinext  31045  mclsppslem  32832  dfpo2  32993  fununiq  33014  slerec  33279  elfix2  33367  poimirlem10  34904  poimirlem11  34905  factwoffsmonot  39105  monotoddzzfi  39546  or2expropbi  43276  dfatcolem  43461  sprsymrelfolem2  43662  poprelb  43693  lindepsnlininds  44514