Theorem breq12 5097

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

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

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breq12i  5101  breq12d  5105  breqan12d  5108  rbropapd  5505  posn  5705  dfrel4  6140  dfpo2  6244  isopolem  7282  poxp  8061  soxp  8062  fnse  8066  poxp2  8076  poxp3  8083  ecopover  8748  canth2g  9048  ttrclss  9616  ttrclselem2  9622  infxpen  9908  sornom  10171  dcomex  10341  zorn2lem6  10395  brdom6disj  10426  fpwwe2  10537  rankcf  10671  ltresr  11034  ltxrlt  11186  wloglei  11652  ltxr  13017  xrltnr  13021  xrltnsym  13039  xrlttri  13041  xrlttr  13042  brfi1uzind  14415  brfi1indALT  14417  f1olecpbl  17431  isfull  17819  isfth  17823  prslem  18203  pslem  18478  dirtr  18508  xrsdsval  21317  dvcvx  25923  2sqmo  27346  2sqreultblem  27357  2sqreunnltblem  27360  2sqreuopb  27377  ssltsn  27703  slerec  27730  addsproplem2  27882  negsproplem2  27940  recut  28365  0reno  28366  axcontlem9  28917  isrusgr  29507  wlk2f  29575  istrlson  29650  upgrwlkdvspth  29684  ispthson  29687  isspthson  29688  crctcshwlk  29767  crctcsh  29769  2pthon3v  29888  umgr2wlk  29894  0pthonv  30073  1pthon2v  30097  uhgr3cyclex  30126  brfinext  33625  finextfldext  33637  bralgext  33670  mclsppslem  35566  fununiq  35752  elfix2  35888  poimirlem10  37620  poimirlem11  37621  dvdsexpnn0  42317  monotoddzzfi  42925  or2expropbi  47028  dfatcolem  47249  sprsymrelfolem2  47487  poprelb  47518  cycldlenngric  47922  gpgprismgr4cyclex  48101  lgricngricex  48123  lindepsnlininds  48447  catprslem  49005