| 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 5146 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
| 2 | breq2 5147 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
| 3 | 1, 2 | sylan9bb 509 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 class class class wbr 5143 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 |
| This theorem is referenced by: breq12i 5152 breq12d 5156 breqan12d 5159 rbropapd 5569 posn 5771 dfrel4 6211 dfpo2 6316 isopolem 7365 poxp 8153 soxp 8154 fnse 8158 poxp2 8168 poxp3 8175 ecopover 8861 canth2g 9171 ttrclss 9760 ttrclselem2 9766 infxpen 10054 sornom 10317 dcomex 10487 zorn2lem6 10541 brdom6disj 10572 fpwwe2 10683 rankcf 10817 ltresr 11180 ltxrlt 11331 wloglei 11795 ltxr 13157 xrltnr 13161 xrltnsym 13179 xrlttri 13181 xrlttr 13182 brfi1uzind 14547 brfi1indALT 14549 f1olecpbl 17572 isfull 17957 isfth 17961 prslem 18343 pslem 18617 dirtr 18647 xrsdsval 21428 dvcvx 26059 2sqmo 27481 2sqreultblem 27492 2sqreunnltblem 27495 2sqreuopb 27512 ssltsn 27837 slerec 27864 addsproplem2 28003 negsproplem2 28061 nohalf 28407 recut 28428 0reno 28429 axcontlem9 28987 isrusgr 29579 wlk2f 29648 istrlson 29725 upgrwlkdvspth 29759 ispthson 29762 isspthson 29763 crctcshwlk 29842 crctcsh 29844 2pthon3v 29963 umgr2wlk 29969 0pthonv 30148 1pthon2v 30172 uhgr3cyclex 30201 brfinext 33704 mclsppslem 35588 fununiq 35769 elfix2 35905 poimirlem10 37637 poimirlem11 37638 factwoffsmonot 42243 dvdsexpnn0 42369 monotoddzzfi 42954 or2expropbi 47046 dfatcolem 47267 sprsymrelfolem2 47480 poprelb 47511 lindepsnlininds 48369 catprslem 48899 |
| Copyright terms: Public domain | W3C validator |