Theorem breq12 5112

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  breq12i  5116  breq12d  5120  breqan12d  5123  rbropapd  5545  posn  5745  dfrel4  6188  dfpo2  6298  isopolem  7349  poxp  8129  soxp  8130  fnse  8134  poxp2  8144  poxp3  8151  ecopover  8824  canth2g  9132  ttrclss  9702  ttrclselem2  9708  infxpen  10020  sornom  10282  dcomex  10452  zorn2lem6  10506  brdom6disj  10538  fpwwe2  10653  rankcf  10787  ltresr  11150  ltxrlt  11305  wloglei  11771  ltxr  13166  xrltnr  13170  xrltnsym  13188  xrlttri  13190  xrlttr  13191  brfi1uzind  14573  brfi1indALT  14575  f1olecpbl  17615  isfull  18003  isfth  18007  prslem  18387  pslem  18662  dirtr  18692  xrsdsval  21623  dvcvx  26247  2sqmo  27669  2sqreultblem  27680  2sqreunnltblem  27683  2sqreuopb  27700  lesrec  28060  addsproplem2  28231  negsproplem2  28290  recut  28755  elreno2  28756  axcontlem9  29413  isrusgr  30005  wlk2f  30073  istrlson  30152  upgrwlkdvspth  30188  ispthson  30191  isspthson  30192  crctcshwlk  30274  crctcsh  30276  2pthon3v  30395  umgr2wlk  30401  0pthonv  30583  1pthon2v  30617  uhgr3cyclex  30646  brfinext  34147  finextfldext  34159  bralgext  34192  mclsppslem  36147  fununiq  36333  elfix2  36466  poimirlem10  38364  poimirlem11  38365  dvdsexpnn0  43194  monotoddzzfi  43768  or2expropbi  47907  dfatcolem  48128  sprsymrelfolem2  48378  poprelb  48409  cycldlenngric  48829  gpgprismgr4cyclex  49008  lgricngricex  49030  lindepsnlininds  49367  catprslem  49921