Theorem breq12 5091

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breq12i  5095  breq12d  5099  breqan12d  5102  rbropapd  5512  posn  5712  dfrel4  6151  dfpo2  6256  isopolem  7295  poxp  8073  soxp  8074  fnse  8078  poxp2  8088  poxp3  8095  ecopover  8763  canth2g  9064  ttrclss  9636  ttrclselem2  9642  infxpen  9931  sornom  10194  dcomex  10364  zorn2lem6  10418  brdom6disj  10449  fpwwe2  10561  rankcf  10695  ltresr  11058  ltxrlt  11211  wloglei  11677  ltxr  13061  xrltnr  13065  xrltnsym  13083  xrlttri  13085  xrlttr  13086  brfi1uzind  14465  brfi1indALT  14467  f1olecpbl  17486  isfull  17874  isfth  17878  prslem  18258  pslem  18533  dirtr  18563  xrsdsval  21404  dvcvx  26001  2sqmo  27418  2sqreultblem  27429  2sqreunnltblem  27432  2sqreuopb  27449  lesrec  27809  addsproplem2  27980  negsproplem2  28039  recut  28504  elreno2  28505  axcontlem9  29059  isrusgr  29649  wlk2f  29717  istrlson  29792  upgrwlkdvspth  29826  ispthson  29829  isspthson  29830  crctcshwlk  29909  crctcsh  29911  2pthon3v  30030  umgr2wlk  30036  0pthonv  30218  1pthon2v  30242  uhgr3cyclex  30271  brfinext  33816  finextfldext  33828  bralgext  33861  mclsppslem  35785  fununiq  35971  elfix2  36104  poimirlem10  37969  poimirlem11  37970  dvdsexpnn0  42784  monotoddzzfi  43392  or2expropbi  47498  dfatcolem  47719  sprsymrelfolem2  47969  poprelb  48000  cycldlenngric  48420  gpgprismgr4cyclex  48599  lgricngricex  48621  lindepsnlininds  48944  catprslem  49501