Theorem breq12 5154

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  breq12i  5158  breq12d  5162  breqan12d  5165  rbropapd  5565  posn  5762  dfrel4  6191  dfpo2  6296  isopolem  7342  poxp  8114  soxp  8115  fnse  8119  poxp2  8129  poxp3  8136  ecopover  8815  canth2g  9131  ttrclss  9715  ttrclselem2  9721  infxpen  10009  sornom  10272  dcomex  10442  zorn2lem6  10496  brdom6disj  10527  fpwwe2  10638  rankcf  10772  ltresr  11135  ltxrlt  11284  wloglei  11746  ltxr  13095  xrltnr  13099  xrltnsym  13116  xrlttri  13118  xrlttr  13119  brfi1uzind  14459  brfi1indALT  14461  f1olecpbl  17473  isfull  17861  isfth  17865  prslem  18251  pslem  18525  dirtr  18555  xrsdsval  20989  dvcvx  25537  2sqmo  26940  2sqreultblem  26951  2sqreunnltblem  26954  2sqreuopb  26971  ssltsn  27294  slerec  27321  addsproplem2  27456  negsproplem2  27506  axcontlem9  28261  isrusgr  28849  wlk2f  28918  istrlson  28995  upgrwlkdvspth  29027  ispthson  29030  isspthson  29031  crctcshwlk  29107  crctcsh  29109  2pthon3v  29228  umgr2wlk  29234  0pthonv  29413  1pthon2v  29437  uhgr3cyclex  29466  brfinext  32763  mclsppslem  34605  fununiq  34771  elfix2  34907  poimirlem10  36546  poimirlem11  36547  factwoffsmonot  41071  dvdsexpnn0  41280  monotoddzzfi  41729  or2expropbi  45792  dfatcolem  46011  sprsymrelfolem2  46209  poprelb  46240  lindepsnlininds  47181  catprslem  47678