![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relco | Structured version Visualization version GIF version |
Description: A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
Ref | Expression |
---|---|
relco | ⊢ Rel (𝐴 ∘ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-co 5459 | . 2 ⊢ (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} | |
2 | 1 | relopabi 5587 | 1 ⊢ Rel (𝐴 ∘ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∃wex 1765 class class class wbr 4968 ∘ ccom 5454 Rel wrel 5455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-rab 3116 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-opab 5031 df-xp 5456 df-rel 5457 df-co 5459 |
This theorem is referenced by: dfco2 5980 resco 5985 coeq0 5990 coiun 5991 cocnvcnv2 5993 cores2 5994 co02 5995 co01 5996 coi1 5997 coass 6000 cossxp 6005 fmptco 6761 cofunexg 7513 dftpos4 7769 wunco 10008 relexprelg 14235 relexpaddg 14250 imasless 16646 znleval 20387 metustexhalf 22853 fcoinver 30043 fmptcof2 30088 dfpo2 32601 cnvco1 32605 cnvco2 32606 opelco3 32628 txpss3v 32950 sscoid 32985 xrnss3v 35176 cononrel1 39460 cononrel2 39461 coiun1 39503 relexpaddss 39569 brco2f1o 39888 brco3f1o 39889 neicvgnvor 39972 sblpnf 40201 |
Copyright terms: Public domain | W3C validator |