![]() |
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 4688 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
2 | breq2 4689 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
3 | 1, 2 | sylan9bb 736 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 class class class wbr 4685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 |
This theorem is referenced by: breq12i 4694 breq12d 4698 breqan12d 4701 rbropapd 5044 posn 5221 dfrel4 5620 isopolem 6635 poxp 7334 soxp 7335 fnse 7339 ecopover 7894 canth2g 8155 infxpen 8875 sornom 9137 dcomex 9307 zorn2lem6 9361 brdom6disj 9392 fpwwe2 9503 rankcf 9637 ltresr 9999 ltxrlt 10146 wloglei 10598 ltxr 11987 xrltnr 11991 xrltnsym 12008 xrlttri 12010 xrlttr 12011 brfi1uzind 13318 brfi1indALT 13320 f1olecpbl 16234 isfull 16617 isfth 16621 prslem 16978 pslem 17253 dirtr 17283 xrsdsval 19838 dvcvx 23828 axcontlem9 25897 isrusgr 26513 wlk2f 26581 istrlson 26659 upgrwlkdvspth 26691 ispthson 26694 isspthson 26695 crctcshwlk 26770 crctcsh 26772 2pthon3v 26908 umgr2wlk 26914 0pthonv 27107 1pthon2v 27131 uhgr3cyclex 27160 2sqmo 29777 mclsppslem 31606 dfpo2 31771 fununiq 31793 slerec 32048 elfix2 32136 poimirlem10 33549 poimirlem11 33550 monotoddzzfi 37824 sprsymrelfolem2 42068 lindepsnlininds 42566 |
Copyright terms: Public domain | W3C validator |