Theorem breq12 4582

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

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474   class class class wbr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578

This theorem is referenced by:  breq12i  4586  breq12d  4590  breqan12d  4593  rbropapd  4928  posn  5099  dfrel4  5489  isopolem  6472  poxp  7153  soxp  7154  fnse  7158  ecopover  7715  ecopoverOLD  7716  canth2g  7976  infxpen  8697  sornom  8959  dcomex  9129  zorn2lem6  9183  brdom6disj  9212  fpwwe2  9321  rankcf  9455  ltresr  9817  ltxrlt  9959  wloglei  10411  ltxr  11786  xrltnr  11792  xrltnsym  11807  xrlttri  11809  xrlttr  11810  brfi1uzind  13083  brfi1indALT  13085  brfi1uzindOLD  13089  brfi1indALTOLD  13091  f1olecpbl  15958  isfull  16341  isfth  16345  prslem  16702  pslem  16977  dirtr  17007  xrsdsval  19557  dvcvx  23531  axcontlem9  25597  iscusgra  25778  sizeusglecusg  25807  iswlkon  25855  istrlon  25864  ispth  25891  isspth  25892  ispthon  25899  0pthonv  25904  isspthon  25906  1pthon2v  25916  2pthon3v  25927  usg2wlk  25938  usg2wlkon  25939  constr3cyclpe  25984  3v3e3cycl2  25985  isclwlk0  26075  isrusgra  26247  iseupa  26285  2sqmo  28773  mclsppslem  30527  dfpo2  30691  fununiq  30706  elfix2  30974  poimirlem10  32372  poimirlem11  32373  monotoddzzfi  36308  isrusgr  40742  1wlk2f  40815  istrlson  40895  upgrwlkdvspth  40926  ispthson  40929  isspthson  40930  crctcsh1wlk  41006  crctcsh  41008  2pthon3v-av  41131  umgr2wlk  41137  0pthonv-av  41278  1pthon2v-av  41301  uhgr3cyclex  41330  lindepsnlininds  42016