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 5590 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
3 | 1, 2 | mpan 690 | 1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2110 Vcvv 3401 class class class wbr 5043 Rel wrel 5545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pr 5311 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2713 df-cleq 2726 df-clel 2812 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3403 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-sn 4532 df-pr 4534 df-op 4538 df-br 5044 df-opab 5106 df-xp 5546 df-rel 5547 |
This theorem is referenced by: nprrel12 5596 vtoclr 5601 relbrcnvg 5962 ovprc 7240 oprabv 7260 encv 8623 fsuppimp 8980 fsuppunbi 8995 brfi1uzind 14047 brfi1indALT 14049 isstruct2 16694 brssc 17291 isfull 17389 isfth 17393 dvdsr 19636 ulmval 25244 subgrv 27330 vcex 28631 opelco3 33437 bj-ideqgALT 35021 bj-idreseqb 35026 bj-ideqg1ALT 35028 rngoablo2 35761 aovprc 44306 aovrcl 44307 nelbrim 44393 isisomgr 44903 linindsv 45413 |
Copyright terms: Public domain | W3C validator |