Theorem breq12 5112

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breq12i  5116  breq12d  5120  breqan12d  5123  rbropapd  5524  posn  5724  dfrel4  6164  dfpo2  6269  isopolem  7320  poxp  8107  soxp  8108  fnse  8112  poxp2  8122  poxp3  8129  ecopover  8794  canth2g  9095  ttrclss  9673  ttrclselem2  9679  infxpen  9967  sornom  10230  dcomex  10400  zorn2lem6  10454  brdom6disj  10485  fpwwe2  10596  rankcf  10730  ltresr  11093  ltxrlt  11244  wloglei  11710  ltxr  13075  xrltnr  13079  xrltnsym  13097  xrlttri  13099  xrlttr  13100  brfi1uzind  14473  brfi1indALT  14475  f1olecpbl  17490  isfull  17874  isfth  17878  prslem  18258  pslem  18531  dirtr  18561  xrsdsval  21327  dvcvx  25925  2sqmo  27348  2sqreultblem  27359  2sqreunnltblem  27362  2sqreuopb  27379  ssltsn  27704  slerec  27731  addsproplem2  27877  negsproplem2  27935  recut  28347  0reno  28348  axcontlem9  28899  isrusgr  29489  wlk2f  29558  istrlson  29635  upgrwlkdvspth  29669  ispthson  29672  isspthson  29673  crctcshwlk  29752  crctcsh  29754  2pthon3v  29873  umgr2wlk  29879  0pthonv  30058  1pthon2v  30082  uhgr3cyclex  30111  brfinext  33648  mclsppslem  35570  fununiq  35756  elfix2  35892  poimirlem10  37624  poimirlem11  37625  dvdsexpnn0  42322  monotoddzzfi  42931  or2expropbi  47035  dfatcolem  47256  sprsymrelfolem2  47494  poprelb  47525  cycldlenngric  47928  gpgprismgr4cyclex  48097  lgricngricex  48119  lindepsnlininds  48441  catprslem  48999