Theorem breq12 5104

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  breq12i  5108  breq12d  5112  breqan12d  5115  rbropapd  5511  posn  5711  dfrel4  6150  dfpo2  6255  isopolem  7293  poxp  8072  soxp  8073  fnse  8077  poxp2  8087  poxp3  8094  ecopover  8762  canth2g  9063  ttrclss  9633  ttrclselem2  9639  infxpen  9928  sornom  10191  dcomex  10361  zorn2lem6  10415  brdom6disj  10446  fpwwe2  10558  rankcf  10692  ltresr  11055  ltxrlt  11207  wloglei  11673  ltxr  13033  xrltnr  13037  xrltnsym  13055  xrlttri  13057  xrlttr  13058  brfi1uzind  14435  brfi1indALT  14437  f1olecpbl  17452  isfull  17840  isfth  17844  prslem  18224  pslem  18499  dirtr  18529  xrsdsval  21369  dvcvx  25985  2sqmo  27408  2sqreultblem  27419  2sqreunnltblem  27422  2sqreuopb  27439  lesrec  27799  addsproplem2  27970  negsproplem2  28029  recut  28494  elreno2  28495  axcontlem9  29049  isrusgr  29639  wlk2f  29707  istrlson  29782  upgrwlkdvspth  29816  ispthson  29819  isspthson  29820  crctcshwlk  29899  crctcsh  29901  2pthon3v  30020  umgr2wlk  30026  0pthonv  30208  1pthon2v  30232  uhgr3cyclex  30261  brfinext  33811  finextfldext  33823  bralgext  33856  mclsppslem  35779  fununiq  35965  elfix2  36098  poimirlem10  37833  poimirlem11  37834  dvdsexpnn0  42656  monotoddzzfi  43251  or2expropbi  47347  dfatcolem  47568  sprsymrelfolem2  47806  poprelb  47837  cycldlenngric  48241  gpgprismgr4cyclex  48420  lgricngricex  48442  lindepsnlininds  48765  catprslem  49322