![]() |
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 4889 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
2 | breq2 4890 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
3 | 1, 2 | sylan9bb 505 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 class class class wbr 4886 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-br 4887 |
This theorem is referenced by: breq12i 4895 breq12d 4899 breqan12d 4902 rbropapd 5252 posn 5435 dfrel4 5839 isopolem 6867 poxp 7570 soxp 7571 fnse 7575 ecopover 8135 canth2g 8402 infxpen 9170 sornom 9434 dcomex 9604 zorn2lem6 9658 brdom6disj 9689 fpwwe2 9800 rankcf 9934 ltresr 10297 ltxrlt 10447 wloglei 10907 ltxr 12260 xrltnr 12264 xrltnsym 12280 xrlttri 12282 xrlttr 12283 brfi1uzind 13594 brfi1indALT 13596 f1olecpbl 16573 isfull 16955 isfth 16959 prslem 17317 pslem 17592 dirtr 17622 xrsdsval 20186 dvcvx 24220 axcontlem9 26321 isrusgr 26909 wlk2f 26977 istrlson 27059 upgrwlkdvspth 27091 ispthson 27094 isspthson 27095 crctcshwlk 27171 crctcsh 27173 2pthon3v 27323 umgr2wlk 27329 0pthonv 27532 1pthon2v 27556 uhgr3cyclex 27585 2sqmo 30211 mclsppslem 32079 dfpo2 32239 fununiq 32260 slerec 32512 elfix2 32600 poimirlem10 34029 poimirlem11 34030 monotoddzzfi 38448 dfatcolem 42278 sprsymrelfolem2 42414 lindepsnlininds 43238 |
Copyright terms: Public domain | W3C validator |