Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > brrelex12i | Structured version Visualization version GIF version |
Description: Two classes that are related by a binary relation are sets. Inference form. (Contributed by BJ, 3-Oct-2022.) |
Ref | Expression |
---|---|
brrelexi.1 | ⊢ Rel 𝑅 |
Ref | Expression |
---|---|
brrelex12i | ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 | . 2 ⊢ Rel 𝑅 | |
2 | brrelex12 5607 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
3 | 1, 2 | mpan 688 | 1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2113 Vcvv 3497 class class class wbr 5069 Rel wrel 5563 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-br 5070 df-opab 5132 df-xp 5564 df-rel 5565 |
This theorem is referenced by: nprrel12 5613 vtoclr 5618 relbrcnvg 5971 ovprc 7197 oprabv 7217 encv 8520 fsuppimp 8842 fsuppunbi 8857 brfi1uzind 13859 isstruct2 16496 brssc 17087 isfull 17183 isfth 17187 dvdsr 19399 ulmval 24971 subgrv 27055 vcex 28358 opelco3 33022 bj-ideqgALT 34454 bj-idreseqb 34459 bj-ideqg1ALT 34461 rngoablo2 35191 aovprc 43394 aovrcl 43395 nelbrim 43481 isisomgr 43996 linindsv 44507 |
Copyright terms: Public domain | W3C validator |