Theorem breq12 5105

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breq12i  5109  breq12d  5113  breqan12d  5116  rbropapd  5520  posn  5720  dfrel4  6159  dfpo2  6264  isopolem  7303  poxp  8082  soxp  8083  fnse  8087  poxp2  8097  poxp3  8104  ecopover  8772  canth2g  9073  ttrclss  9643  ttrclselem2  9649  infxpen  9938  sornom  10201  dcomex  10371  zorn2lem6  10425  brdom6disj  10456  fpwwe2  10568  rankcf  10702  ltresr  11065  ltxrlt  11217  wloglei  11683  ltxr  13043  xrltnr  13047  xrltnsym  13065  xrlttri  13067  xrlttr  13068  brfi1uzind  14445  brfi1indALT  14447  f1olecpbl  17462  isfull  17850  isfth  17854  prslem  18234  pslem  18509  dirtr  18539  xrsdsval  21382  dvcvx  25998  2sqmo  27421  2sqreultblem  27432  2sqreunnltblem  27435  2sqreuopb  27452  lesrec  27812  addsproplem2  27983  negsproplem2  28042  recut  28507  elreno2  28508  axcontlem9  29063  isrusgr  29653  wlk2f  29721  istrlson  29796  upgrwlkdvspth  29830  ispthson  29833  isspthson  29834  crctcshwlk  29913  crctcsh  29915  2pthon3v  30034  umgr2wlk  30040  0pthonv  30222  1pthon2v  30246  uhgr3cyclex  30275  brfinext  33836  finextfldext  33848  bralgext  33881  mclsppslem  35805  fununiq  35991  elfix2  36124  poimirlem10  37910  poimirlem11  37911  dvdsexpnn0  42733  monotoddzzfi  43328  or2expropbi  47423  dfatcolem  47644  sprsymrelfolem2  47882  poprelb  47913  cycldlenngric  48317  gpgprismgr4cyclex  48496  lgricngricex  48518  lindepsnlininds  48841  catprslem  49398