Theorem breq12 5094

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  breq12i  5098  breq12d  5102  breqan12d  5105  rbropapd  5500  posn  5700  dfrel4  6138  dfpo2  6243  isopolem  7279  poxp  8058  soxp  8059  fnse  8063  poxp2  8073  poxp3  8080  ecopover  8745  canth2g  9044  ttrclss  9610  ttrclselem2  9616  infxpen  9905  sornom  10168  dcomex  10338  zorn2lem6  10392  brdom6disj  10423  fpwwe2  10534  rankcf  10668  ltresr  11031  ltxrlt  11183  wloglei  11649  ltxr  13014  xrltnr  13018  xrltnsym  13036  xrlttri  13038  xrlttr  13039  brfi1uzind  14415  brfi1indALT  14417  f1olecpbl  17431  isfull  17819  isfth  17823  prslem  18203  pslem  18478  dirtr  18508  xrsdsval  21347  dvcvx  25952  2sqmo  27375  2sqreultblem  27386  2sqreunnltblem  27389  2sqreuopb  27406  slerec  27760  addsproplem2  27913  negsproplem2  27971  recut  28398  0reno  28399  axcontlem9  28950  isrusgr  29540  wlk2f  29608  istrlson  29683  upgrwlkdvspth  29717  ispthson  29720  isspthson  29721  crctcshwlk  29800  crctcsh  29802  2pthon3v  29921  umgr2wlk  29927  0pthonv  30109  1pthon2v  30133  uhgr3cyclex  30162  brfinext  33665  finextfldext  33677  bralgext  33710  mclsppslem  35627  fununiq  35813  elfix2  35946  poimirlem10  37669  poimirlem11  37670  dvdsexpnn0  42426  monotoddzzfi  43034  or2expropbi  47133  dfatcolem  47354  sprsymrelfolem2  47592  poprelb  47623  cycldlenngric  48027  gpgprismgr4cyclex  48206  lgricngricex  48228  lindepsnlininds  48552  catprslem  49110