Theorem breq12 5115

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  breq12i  5119  breq12d  5123  breqan12d  5126  rbropapd  5527  posn  5727  dfrel4  6167  dfpo2  6272  isopolem  7323  poxp  8110  soxp  8111  fnse  8115  poxp2  8125  poxp3  8132  ecopover  8797  canth2g  9101  ttrclss  9680  ttrclselem2  9686  infxpen  9974  sornom  10237  dcomex  10407  zorn2lem6  10461  brdom6disj  10492  fpwwe2  10603  rankcf  10737  ltresr  11100  ltxrlt  11251  wloglei  11717  ltxr  13082  xrltnr  13086  xrltnsym  13104  xrlttri  13106  xrlttr  13107  brfi1uzind  14480  brfi1indALT  14482  f1olecpbl  17497  isfull  17881  isfth  17885  prslem  18265  pslem  18538  dirtr  18568  xrsdsval  21334  dvcvx  25932  2sqmo  27355  2sqreultblem  27366  2sqreunnltblem  27369  2sqreuopb  27386  ssltsn  27711  slerec  27738  addsproplem2  27884  negsproplem2  27942  recut  28354  0reno  28355  axcontlem9  28906  isrusgr  29496  wlk2f  29565  istrlson  29642  upgrwlkdvspth  29676  ispthson  29679  isspthson  29680  crctcshwlk  29759  crctcsh  29761  2pthon3v  29880  umgr2wlk  29886  0pthonv  30065  1pthon2v  30089  uhgr3cyclex  30118  brfinext  33655  mclsppslem  35577  fununiq  35763  elfix2  35899  poimirlem10  37631  poimirlem11  37632  dvdsexpnn0  42329  monotoddzzfi  42938  or2expropbi  47039  dfatcolem  47260  sprsymrelfolem2  47498  poprelb  47529  cycldlenngric  47932  gpgprismgr4cyclex  48101  lgricngricex  48123  lindepsnlininds  48445  catprslem  49003