Theorem breq12 4891

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   class class class wbr 4886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4887

This theorem is referenced by:  breq12i  4895  breq12d  4899  breqan12d  4902  rbropapd  5252  posn  5435  dfrel4  5839  isopolem  6867  poxp  7570  soxp  7571  fnse  7575  ecopover  8135  canth2g  8402  infxpen  9170  sornom  9434  dcomex  9604  zorn2lem6  9658  brdom6disj  9689  fpwwe2  9800  rankcf  9934  ltresr  10297  ltxrlt  10447  wloglei  10907  ltxr  12260  xrltnr  12264  xrltnsym  12280  xrlttri  12282  xrlttr  12283  brfi1uzind  13594  brfi1indALT  13596  f1olecpbl  16573  isfull  16955  isfth  16959  prslem  17317  pslem  17592  dirtr  17622  xrsdsval  20186  dvcvx  24220  axcontlem9  26321  isrusgr  26909  wlk2f  26977  istrlson  27059  upgrwlkdvspth  27091  ispthson  27094  isspthson  27095  crctcshwlk  27171  crctcsh  27173  2pthon3v  27323  umgr2wlk  27329  0pthonv  27532  1pthon2v  27556  uhgr3cyclex  27585  2sqmo  30211  mclsppslem  32079  dfpo2  32239  fununiq  32260  slerec  32512  elfix2  32600  poimirlem10  34029  poimirlem11  34030  monotoddzzfi  38448  dfatcolem  42278  sprsymrelfolem2  42414  lindepsnlininds  43238