Theorem breq12 5107

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  breq12i  5111  breq12d  5115  breqan12d  5118  rbropapd  5535  posn  5735  dfrel4  6179  dfpo2  6285  isopolem  7331  poxp  8110  soxp  8111  fnse  8115  poxp2  8125  poxp3  8132  ecopover  8805  canth2g  9105  ttrclss  9677  ttrclselem2  9683  infxpen  9972  sornom  10236  dcomex  10406  zorn2lem6  10460  brdom6disj  10491  fpwwe2  10603  rankcf  10737  ltresr  11100  ltxrlt  11255  wloglei  11721  ltxr  13119  xrltnr  13123  xrltnsym  13141  xrlttri  13143  xrlttr  13144  brfi1uzind  14523  brfi1indALT  14525  f1olecpbl  17559  isfull  17947  isfth  17951  prslem  18331  pslem  18606  dirtr  18636  xrsdsval  21465  dvcvx  26084  2sqmo  27503  2sqreultblem  27514  2sqreunnltblem  27517  2sqreuopb  27534  lesrec  27894  addsproplem2  28065  negsproplem2  28124  recut  28589  elreno2  28590  axcontlem9  29175  isrusgr  29764  wlk2f  29832  istrlson  29907  upgrwlkdvspth  29941  ispthson  29944  isspthson  29945  crctcshwlk  30024  crctcsh  30026  2pthon3v  30145  umgr2wlk  30151  0pthonv  30333  1pthon2v  30357  uhgr3cyclex  30386  brfinext  33951  finextfldext  33963  bralgext  33996  mclsppslem  35938  fununiq  36124  elfix2  36257  poimirlem10  38134  poimirlem11  38135  dvdsexpnn0  42948  monotoddzzfi  43524  or2expropbi  47633  dfatcolem  47854  sprsymrelfolem2  48104  poprelb  48135  cycldlenngric  48555  gpgprismgr4cyclex  48734  lgricngricex  48756  lindepsnlininds  49079  catprslem  49636