![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > releq | Structured version Visualization version GIF version |
Description: Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
releq | ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1 3822 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V))) | |
2 | df-rel 5319 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
3 | df-rel 5319 | . 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
4 | 1, 2, 3 | 3bitr4g 306 | 1 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1653 Vcvv 3385 ⊆ wss 3769 × cxp 5310 Rel wrel 5317 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-in 3776 df-ss 3783 df-rel 5319 |
This theorem is referenced by: releqi 5407 releqd 5408 dfrel2 5800 tposfn2 7612 ereq1 7989 isps 17517 isdir 17547 fpwrelmapffslem 30025 bnj1321 31612 cnfinltrel 33739 refreleq 34764 symreleq 34798 trreleq 34822 prtlem12 34888 relintabex 38666 clrellem 38708 clcnvlem 38709 |
Copyright terms: Public domain | W3C validator |