![]() |
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 4005 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V))) | |
2 | df-rel 5689 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
3 | df-rel 5689 | . 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
4 | 1, 2, 3 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 Vcvv 3462 ⊆ wss 3947 × cxp 5680 Rel wrel 5687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ss 3964 df-rel 5689 |
This theorem is referenced by: releqi 5783 releqd 5784 relsnb 5808 dfrel2 6200 tposfn2 8263 ereq1 8741 isps 18593 isdir 18623 fpwrelmapffslem 32646 bnj1321 34872 refreleq 38219 symreleq 38256 trreleq 38280 prtlem12 38565 relintabex 43248 clrellem 43289 clcnvlem 43290 |
Copyright terms: Public domain | W3C validator |