Theorem breq12 5080

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  breq12i  5084  breq12d  5088  breqan12d  5091  rbropapd  5507  posn  5707  dfrel4  6146  dfpo2  6251  isopolem  7293  poxp  8072  soxp  8073  fnse  8077  poxp2  8087  poxp3  8094  ecopover  8762  canth2g  9063  ttrclss  9636  ttrclselem2  9642  infxpen  9931  sornom  10194  dcomex  10364  zorn2lem6  10418  brdom6disj  10449  fpwwe2  10561  rankcf  10695  ltresr  11058  ltxrlt  11211  wloglei  11677  ltxr  13061  xrltnr  13065  xrltnsym  13083  xrlttri  13085  xrlttr  13086  brfi1uzind  14465  brfi1indALT  14467  f1olecpbl  17486  isfull  17874  isfth  17878  prslem  18258  pslem  18533  dirtr  18563  xrsdsval  21390  dvcvx  26009  2sqmo  27422  2sqreultblem  27433  2sqreunnltblem  27436  2sqreuopb  27453  lesrec  27813  addsproplem2  27984  negsproplem2  28043  recut  28508  elreno2  28509  axcontlem9  29063  isrusgr  29652  wlk2f  29720  istrlson  29795  upgrwlkdvspth  29829  ispthson  29832  isspthson  29833  crctcshwlk  29912  crctcsh  29914  2pthon3v  30033  umgr2wlk  30039  0pthonv  30221  1pthon2v  30245  uhgr3cyclex  30274  brfinext  33848  finextfldext  33860  bralgext  33893  mclsppslem  35826  fununiq  36012  elfix2  36145  poimirlem10  38012  poimirlem11  38013  dvdsexpnn0  42826  monotoddzzfi  43402  or2expropbi  47511  dfatcolem  47732  sprsymrelfolem2  47982  poprelb  48013  cycldlenngric  48433  gpgprismgr4cyclex  48612  lgricngricex  48634  lindepsnlininds  48957  catprslem  49514