Theorem breq12 4588

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  breq12i  4592  breq12d  4596  breqan12d  4599  rbropapd  4939  posn  5110  dfrel4  5504  isopolem  6495  poxp  7176  soxp  7177  fnse  7181  ecopover  7738  ecopoverOLD  7739  canth2g  7999  infxpen  8720  sornom  8982  dcomex  9152  zorn2lem6  9206  brdom6disj  9235  fpwwe2  9344  rankcf  9478  ltresr  9840  ltxrlt  9987  wloglei  10439  ltxr  11825  xrltnr  11829  xrltnsym  11846  xrlttri  11848  xrlttr  11849  brfi1uzind  13135  brfi1indALT  13137  brfi1uzindOLD  13141  brfi1indALTOLD  13143  f1olecpbl  16010  isfull  16393  isfth  16397  prslem  16754  pslem  17029  dirtr  17059  xrsdsval  19609  dvcvx  23587  axcontlem9  25652  iscusgra  25985  sizeusglecusg  26014  iswlkon  26062  istrlon  26071  ispth  26098  isspth  26099  ispthon  26106  0pthonv  26111  isspthon  26113  1pthon2v  26123  2pthon3v  26134  usg2wlk  26145  usg2wlkon  26146  constr3cyclpe  26191  3v3e3cycl2  26192  isclwlk0  26282  isrusgra  26454  iseupa  26492  2sqmo  28980  mclsppslem  30734  dfpo2  30898  fununiq  30913  elfix2  31181  poimirlem10  32589  poimirlem11  32590  monotoddzzfi  36525  isrusgr  40761  1wlk2f  40834  istrlson  40914  upgrwlkdvspth  40945  ispthson  40948  isspthson  40949  crctcsh1wlk  41025  crctcsh  41027  2pthon3v-av  41150  umgr2wlk  41156  0pthonv-av  41297  1pthon2v-av  41320  uhgr3cyclex  41349  lindepsnlininds  42035