Theorem breq12 5118

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  breq12i  5122  breq12d  5126  breqan12d  5129  rbropapd  5550  posn  5750  dfrel4  6192  dfpo2  6300  isopolem  7346  poxp  8126  soxp  8127  fnse  8131  poxp2  8141  poxp3  8148  ecopover  8821  canth2g  9121  ttrclss  9691  ttrclselem2  9697  infxpen  10000  sornom  10263  dcomex  10433  zorn2lem6  10487  brdom6disj  10518  fpwwe2  10630  rankcf  10764  ltresr  11127  ltxrlt  11282  wloglei  11748  ltxr  13142  xrltnr  13146  xrltnsym  13164  xrlttri  13166  xrlttr  13167  brfi1uzind  14547  brfi1indALT  14549  f1olecpbl  17583  isfull  17971  isfth  17975  prslem  18355  pslem  18630  dirtr  18660  xrsdsval  21532  dvcvx  26150  2sqmo  27569  2sqreultblem  27580  2sqreunnltblem  27583  2sqreuopb  27600  lesrec  27960  addsproplem2  28131  negsproplem2  28190  recut  28655  elreno2  28656  axcontlem9  29265  isrusgr  29854  wlk2f  29922  istrlson  29997  upgrwlkdvspth  30031  ispthson  30034  isspthson  30035  crctcshwlk  30114  crctcsh  30116  2pthon3v  30235  umgr2wlk  30241  0pthonv  30423  1pthon2v  30447  uhgr3cyclex  30476  brfinext  33989  finextfldext  34001  bralgext  34034  mclsppslem  36010  fununiq  36196  elfix2  36329  poimirlem10  38206  poimirlem11  38207  dvdsexpnn0  43022  monotoddzzfi  43598  or2expropbi  47697  dfatcolem  47918  sprsymrelfolem2  48168  poprelb  48199  cycldlenngric  48619  gpgprismgr4cyclex  48798  lgricngricex  48820  lindepsnlininds  49154  catprslem  49710