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 519	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  breq12i  5111  breq12d  5115  breqan12d  5118  rbropapd  5536  posn  5736  dfrel4  6182  dfpo2  6299  fununiq  6555  isopolem  7353  poxp  8140  soxp  8141  fnse  8150  poxp2  8160  poxp3  8167  ecopover  8842  canth2g  9150  ttrclss  9721  ttrclselem2  9727  infxpen  10093  sornom  10355  dcomex  10525  zorn2lem6  10579  brdom6disj  10611  fpwwe2  10728  rankcf  10862  ltresr  11225  ltxrlt  11380  wloglei  11848  ltxr  13244  xrltnr  13248  xrltnsym  13266  xrlttri  13268  xrlttr  13269  brfi1uzind  14653  brfi1indALT  14655  f1olecpbl  17699  isfull  18087  isfth  18091  prslem  18471  pslem  18746  dirtr  18776  xrsdsval  21717  dvcvx  26340  2sqmo  27764  2sqreultblem  27775  2sqreunnltblem  27778  2sqreuopb  27795  lesrec  28185  addsproplem2  28356  negsproplem2  28415  recut  28880  elreno2  28881  axcontlem9  29550  isrusgr  30142  wlk2f  30210  istrlson  30289  upgrwlkdvspth  30325  ispthson  30328  isspthson  30329  crctcshwlk  30411  crctcsh  30413  2pthon3v  30532  umgr2wlk  30538  0pthonv  30720  1pthon2v  30754  uhgr3cyclex  30783  brfinext  34284  finextfldext  34296  bralgext  34329  mclsppslem  36348  elfix2  36666  poimirlem10  38549  poimirlem11  38550  dvdsexpnn0  43387  monotoddzzfi  43949  or2expropbi  48104  dfatcolem  48325  sprsymrelfolem2  48575  poprelb  48606  cycldlenngric  49026  gpgprismgr4cyclex  49205  lgricngricex  49227  lindepsnlininds  49564  catprslem  50118