| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > releqd | Structured version Visualization version GIF version | ||
| Description: Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.) |
| Ref | Expression |
|---|---|
| releqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| releqd | ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | releqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | releq 5786 | . 2 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ 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: dftpos3 8269 tposfo2 8274 tposf12 8276 relexp0rel 15076 relexprelg 15077 relexpreld 15079 relexpaddg 15092 imasaddfnlem 17573 imasvscafn 17582 cicer 17850 joindmss 18424 meetdmss 18438 mattpostpos 22460 cnextrel 24071 perpln1 28718 perpln2 28719 erler 33269 opprabs 33510 relfae 34248 satfrel 35372 dibvalrel 41165 dicvalrelN 41187 diclspsn 41196 dihvalrel 41281 dih1 41288 dihmeetlem4preN 41308 |
| Copyright terms: Public domain | W3C validator |