![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breq12 | Structured version Visualization version GIF version |
Description: Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.) |
Ref | Expression |
---|---|
breq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 5152 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
2 | breq2 5153 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
3 | 1, 2 | sylan9bb 508 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 class class class wbr 5149 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 |
This theorem is referenced by: breq12i 5158 breq12d 5162 breqan12d 5165 rbropapd 5566 posn 5763 dfrel4 6197 dfpo2 6302 isopolem 7352 poxp 8133 soxp 8134 fnse 8138 poxp2 8148 poxp3 8155 ecopover 8840 canth2g 9159 ttrclss 9750 ttrclselem2 9756 infxpen 10044 sornom 10307 dcomex 10477 zorn2lem6 10531 brdom6disj 10562 fpwwe2 10673 rankcf 10807 ltresr 11170 ltxrlt 11321 wloglei 11783 ltxr 13135 xrltnr 13139 xrltnsym 13156 xrlttri 13158 xrlttr 13159 brfi1uzind 14500 brfi1indALT 14502 f1olecpbl 17517 isfull 17907 isfth 17911 prslem 18298 pslem 18572 dirtr 18602 xrsdsval 21365 dvcvx 26002 2sqmo 27420 2sqreultblem 27431 2sqreunnltblem 27434 2sqreuopb 27451 ssltsn 27776 slerec 27803 addsproplem2 27938 negsproplem2 27992 recut 28301 0reno 28302 axcontlem9 28860 isrusgr 29452 wlk2f 29521 istrlson 29598 upgrwlkdvspth 29630 ispthson 29633 isspthson 29634 crctcshwlk 29710 crctcsh 29712 2pthon3v 29831 umgr2wlk 29837 0pthonv 30016 1pthon2v 30040 uhgr3cyclex 30069 brfinext 33478 mclsppslem 35326 fununiq 35497 elfix2 35633 poimirlem10 37236 poimirlem11 37237 factwoffsmonot 41830 dvdsexpnn0 42038 monotoddzzfi 42507 or2expropbi 46556 dfatcolem 46775 sprsymrelfolem2 46972 poprelb 47003 lindepsnlininds 47708 catprslem 48204 |
Copyright terms: Public domain | W3C validator |