Theorem breq12 5107

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breq12i  5111  breq12d  5115  breqan12d  5118  rbropapd  5517  posn  5717  dfrel4  6152  dfpo2  6257  isopolem  7302  poxp  8084  soxp  8085  fnse  8089  poxp2  8099  poxp3  8106  ecopover  8771  canth2g  9072  ttrclss  9649  ttrclselem2  9655  infxpen  9943  sornom  10206  dcomex  10376  zorn2lem6  10430  brdom6disj  10461  fpwwe2  10572  rankcf  10706  ltresr  11069  ltxrlt  11220  wloglei  11686  ltxr  13051  xrltnr  13055  xrltnsym  13073  xrlttri  13075  xrlttr  13076  brfi1uzind  14449  brfi1indALT  14451  f1olecpbl  17466  isfull  17854  isfth  17858  prslem  18238  pslem  18513  dirtr  18543  xrsdsval  21352  dvcvx  25958  2sqmo  27381  2sqreultblem  27392  2sqreunnltblem  27395  2sqreuopb  27412  ssltsn  27738  slerec  27765  addsproplem2  27917  negsproplem2  27975  recut  28400  0reno  28401  axcontlem9  28952  isrusgr  29542  wlk2f  29610  istrlson  29685  upgrwlkdvspth  29719  ispthson  29722  isspthson  29723  crctcshwlk  29802  crctcsh  29804  2pthon3v  29923  umgr2wlk  29929  0pthonv  30108  1pthon2v  30132  uhgr3cyclex  30161  brfinext  33641  mclsppslem  35563  fununiq  35749  elfix2  35885  poimirlem10  37617  poimirlem11  37618  dvdsexpnn0  42315  monotoddzzfi  42924  or2expropbi  47028  dfatcolem  47249  sprsymrelfolem2  47487  poprelb  47518  cycldlenngric  47921  gpgprismgr4cyclex  48090  lgricngricex  48112  lindepsnlininds  48434  catprslem  48992