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 5061 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
2 | breq2 5062 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
3 | 1, 2 | sylan9bb 510 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 class class class wbr 5058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 |
This theorem is referenced by: breq12i 5067 breq12d 5071 breqan12d 5074 rbropapd 5441 posn 5631 dfrel4 6042 isopolem 7087 poxp 7813 soxp 7814 fnse 7818 ecopover 8391 canth2g 8660 infxpen 9429 sornom 9688 dcomex 9858 zorn2lem6 9912 brdom6disj 9943 fpwwe2 10054 rankcf 10188 ltresr 10551 ltxrlt 10700 wloglei 11161 ltxr 12500 xrltnr 12504 xrltnsym 12520 xrlttri 12522 xrlttr 12523 brfi1uzind 13846 brfi1indALT 13848 f1olecpbl 16790 isfull 17170 isfth 17174 prslem 17531 pslem 17806 dirtr 17836 xrsdsval 20519 dvcvx 24546 2sqmo 25941 2sqreultblem 25952 2sqreunnltblem 25955 2sqreuopb 25972 axcontlem9 26686 isrusgr 27271 wlk2f 27339 istrlson 27416 upgrwlkdvspth 27448 ispthson 27451 isspthson 27452 crctcshwlk 27528 crctcsh 27530 2pthon3v 27650 umgr2wlk 27656 0pthonv 27836 1pthon2v 27860 uhgr3cyclex 27889 brfinext 30943 mclsppslem 32728 dfpo2 32889 fununiq 32910 slerec 33175 elfix2 33263 poimirlem10 34784 poimirlem11 34785 monotoddzzfi 39419 or2expropbi 43150 dfatcolem 43335 sprsymrelfolem2 43502 poprelb 43533 lindepsnlininds 44405 |
Copyright terms: Public domain | W3C validator |