| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > releqi | Structured version Visualization version GIF version | ||
| Description: Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.) |
| Ref | Expression |
|---|---|
| releqi.1 | ⊢ 𝐴 = 𝐵 |
| Ref | Expression |
|---|---|
| releqi | ⊢ (Rel 𝐴 ↔ Rel 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | releqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | releq 5786 | . 2 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (Rel 𝐴 ↔ Rel 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 Rel wrel 5690 |
| 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-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-rel 5692 |
| This theorem is referenced by: reliun 5826 reluni 5828 relint 5829 reldmmpo 7567 frrlem6 8316 wfrrelOLD 8354 tfrlem6 8422 relsdom 8992 0rest 17474 firest 17477 2oppchomf 17767 oppchofcl 18305 oyoncl 18315 releqg 19193 reldvdsr 20360 restbas 23166 hlimcaui 31255 gonan0 35397 satffunlem2lem2 35411 relbigcup 35898 fnsingle 35920 funimage 35929 colinrel 36058 brcnvrabga 38343 relcoels 38425 iscard4 43546 neicvgnvor 44129 xlimrel 45835 tposideq2 48789 reldmxpc 48952 |
| Copyright terms: Public domain | W3C validator |