Theorem breq12 5118

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  breq12i  5122  breq12d  5126  breqan12d  5129  rbropapd  5548  posn  5748  dfrel4  6190  dfpo2  6298  isopolem  7344  poxp  8124  soxp  8125  fnse  8129  poxp2  8139  poxp3  8146  ecopover  8819  canth2g  9119  ttrclss  9689  ttrclselem2  9695  infxpen  9998  sornom  10261  dcomex  10431  zorn2lem6  10485  brdom6disj  10516  fpwwe2  10628  rankcf  10762  ltresr  11125  ltxrlt  11280  wloglei  11746  ltxr  13140  xrltnr  13144  xrltnsym  13162  xrlttri  13164  xrlttr  13165  brfi1uzind  14545  brfi1indALT  14547  f1olecpbl  17581  isfull  17969  isfth  17973  prslem  18353  pslem  18628  dirtr  18658  xrsdsval  21530  dvcvx  26148  2sqmo  27567  2sqreultblem  27578  2sqreunnltblem  27581  2sqreuopb  27598  lesrec  27958  addsproplem2  28129  negsproplem2  28188  recut  28653  elreno2  28654  axcontlem9  29263  isrusgr  29852  wlk2f  29920  istrlson  29995  upgrwlkdvspth  30029  ispthson  30032  isspthson  30033  crctcshwlk  30112  crctcsh  30114  2pthon3v  30233  umgr2wlk  30239  0pthonv  30421  1pthon2v  30445  uhgr3cyclex  30474  brfinext  33987  finextfldext  33999  bralgext  34032  mclsppslem  36008  fununiq  36194  elfix2  36327  poimirlem10  38203  poimirlem11  38204  dvdsexpnn0  43019  monotoddzzfi  43595  or2expropbi  47694  dfatcolem  47915  sprsymrelfolem2  48165  poprelb  48196  cycldlenngric  48616  gpgprismgr4cyclex  48795  lgricngricex  48817  lindepsnlininds  49151  catprslem  49707