Theorem breq12 5171

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  breq12i  5175  breq12d  5179  breqan12d  5182  rbropapd  5583  posn  5785  dfrel4  6222  dfpo2  6327  isopolem  7381  poxp  8169  soxp  8170  fnse  8174  poxp2  8184  poxp3  8191  ecopover  8879  canth2g  9197  ttrclss  9789  ttrclselem2  9795  infxpen  10083  sornom  10346  dcomex  10516  zorn2lem6  10570  brdom6disj  10601  fpwwe2  10712  rankcf  10846  ltresr  11209  ltxrlt  11360  wloglei  11822  ltxr  13178  xrltnr  13182  xrltnsym  13199  xrlttri  13201  xrlttr  13202  brfi1uzind  14557  brfi1indALT  14559  f1olecpbl  17587  isfull  17977  isfth  17981  prslem  18368  pslem  18642  dirtr  18672  xrsdsval  21451  dvcvx  26079  2sqmo  27499  2sqreultblem  27510  2sqreunnltblem  27513  2sqreuopb  27530  ssltsn  27855  slerec  27882  addsproplem2  28021  negsproplem2  28079  nohalf  28425  recut  28446  0reno  28447  axcontlem9  29005  isrusgr  29597  wlk2f  29666  istrlson  29743  upgrwlkdvspth  29775  ispthson  29778  isspthson  29779  crctcshwlk  29855  crctcsh  29857  2pthon3v  29976  umgr2wlk  29982  0pthonv  30161  1pthon2v  30185  uhgr3cyclex  30214  brfinext  33666  fldext2chn  33719  mclsppslem  35551  fununiq  35732  elfix2  35868  poimirlem10  37590  poimirlem11  37591  factwoffsmonot  42199  dvdsexpnn0  42321  monotoddzzfi  42899  or2expropbi  46949  dfatcolem  47170  sprsymrelfolem2  47367  poprelb  47398  lindepsnlininds  48181  catprslem  48677