Theorem breq12 5090

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  breq12i  5094  breq12d  5098  breqan12d  5101  rbropapd  5517  posn  5717  dfrel4  6155  dfpo2  6260  isopolem  7300  poxp  8078  soxp  8079  fnse  8083  poxp2  8093  poxp3  8100  ecopover  8768  canth2g  9069  ttrclss  9641  ttrclselem2  9647  infxpen  9936  sornom  10199  dcomex  10369  zorn2lem6  10423  brdom6disj  10454  fpwwe2  10566  rankcf  10700  ltresr  11063  ltxrlt  11216  wloglei  11682  ltxr  13066  xrltnr  13070  xrltnsym  13088  xrlttri  13090  xrlttr  13091  brfi1uzind  14470  brfi1indALT  14472  f1olecpbl  17491  isfull  17879  isfth  17883  prslem  18263  pslem  18538  dirtr  18568  xrsdsval  21391  dvcvx  25987  2sqmo  27400  2sqreultblem  27411  2sqreunnltblem  27414  2sqreuopb  27431  lesrec  27791  addsproplem2  27962  negsproplem2  28021  recut  28486  elreno2  28487  axcontlem9  29041  isrusgr  29630  wlk2f  29698  istrlson  29773  upgrwlkdvspth  29807  ispthson  29810  isspthson  29811  crctcshwlk  29890  crctcsh  29892  2pthon3v  30011  umgr2wlk  30017  0pthonv  30199  1pthon2v  30223  uhgr3cyclex  30252  brfinext  33796  finextfldext  33808  bralgext  33841  mclsppslem  35765  fununiq  35951  elfix2  36084  poimirlem10  37951  poimirlem11  37952  dvdsexpnn0  42766  monotoddzzfi  43370  or2expropbi  47482  dfatcolem  47703  sprsymrelfolem2  47953  poprelb  47984  cycldlenngric  48404  gpgprismgr4cyclex  48583  lgricngricex  48605  lindepsnlininds  48928  catprslem  49485